Metamath Proof Explorer

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 -> ph )
Assertion eqcoms 
|- ( B = A -> ph )

Proof

Step Hyp Ref Expression
1 eqcoms.1 
 |-  ( A = B -> ph )
2 eqcom 
 |-  ( B = A <-> A = B )
3 2 1 sylbi 
 |-  ( B = A -> ph )