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	⊢ ( 𝑥 = 𝑦 → 𝜑 )
Assertion	equcoms	⊢ ( 𝑦 = 𝑥 → 𝜑 )

Proof

Step	Hyp	Ref	Expression
1		equcoms.1	⊢ ( 𝑥 = 𝑦 → 𝜑 )
2		equcomi	⊢ ( 𝑦 = 𝑥 → 𝑥 = 𝑦 )
3	2 1	syl	⊢ ( 𝑦 = 𝑥 → 𝜑 )