Theorem equcoms

An inference commuting equality in antecedent. Used to eliminate the need for a syllogism. (Contributed by NM, 10-Jan-1993.)

Hypothesis
equcoms.1
\( \vdash x' = y' \rightarrow \varphi \)
Conclusion
\( \vdash y' = x' \rightarrow \varphi \)
Proof
l0
equcomi
\( \vdash y' = x' \rightarrow x' = y' \)
equcoms.1
\( \vdash x' = y' \rightarrow \varphi \)
syl l0 _