Theorem eqcoms

Description: Inference applying commutative law for class equality to an antecedent. (Contributed by NM, 24-Jun-1993)

	Ref	Expression
Hypothesis	eqcoms.1	$$⊢A=B\to \phi$$
Assertion	eqcoms	$$⊢B=A\to \phi$$

Proof

Step	Hyp	Ref	Expression
1		eqcoms.1	$$⊢A=B\to \phi$$
2		eqcom	$$⊢B=A\leftrightarrow A=B$$
3	2 1	sylbi	$$⊢B=A\to \phi$$