Theorem equcoms

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

	Ref	Expression
Hypothesis	equcoms.1	$$⊢x=y\to \phi$$
Assertion	equcoms	$$⊢y=x\to \phi$$

Proof

Step	Hyp	Ref	Expression
1		equcoms.1	$$⊢x=y\to \phi$$
2		equcomi	$$⊢y=x\to x=y$$
3	2 1	syl	$$⊢y=x\to \phi$$