Theorem equcomd

Deduction form of equcom, symmetry of equality. For the versions for classes, see [eqcom] and [eqcomd]. (Contributed by BJ, 6-Oct-2019.)

Hypothesis
equcomd.1
\( \vdash \varphi \rightarrow x' = y' \)
Conclusion
\( \vdash \varphi \rightarrow y' = x' \)
Proof
l0
equcomd.1
\( \vdash \varphi \rightarrow x' = y' \)
equcom
\( \vdash x' = y' \leftrightarrow y' = x' \)
sylib l0 _