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 -> ph )
Assertion	equcoms	|- ( y = x -> ph )

Proof

Step	Hyp	Ref	Expression
1		equcoms.1	|- ( x = y -> ph )
2		equcomi	|- ( y = x -> x = y )
3	2 1	syl	|- ( y = x -> ph )