Theorem equcomi

Commutative law for equality. Equality is a symmetric relation. Lemma 3 of [KalishMontague] p. 85. See also Lemma 7 of [Tarski] p. 69. (Contributed by NM, 10-Jan-1993.) (Revised by NM, 9-Apr-2017.)

Conclusion
\( \vdash x' = y' \rightarrow y' = x' \)
Proof
l0
equid
\( \vdash x' = x' \)
ax7
\( \vdash x' = y' \rightarrow x' = x' \rightarrow y' = x' \)
mpi l0 _