Theorem eqcoms 2196

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

Hypothesis

Ref	Expression
eqcoms.1	|- ( A = B -> ph )

Assertion

Ref	Expression
eqcoms	|- ( B = A -> ph )

Proof of Theorem eqcoms

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

Syntax hints:   -> wi 4   = wceq 1364

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1458  ax-gen 1460  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-cleq 2186

This theorem is referenced by:  gencbvex  2806  gencbval  2808  sbceq2a  2996  eqimss2  3234  uneqdifeqim  3532  tppreq3  3721  copsex2t  4274  copsex2g  4275  ordsoexmid  4594  0elsucexmid  4597  ordpwsucexmid  4602  cnveqb  5121  cnveq0  5122  relcoi1  5197  funtpg  5305  f0rn0  5448  fimadmfo  5485  f1ocnvfv  5822  f1ocnvfvb  5823  cbvfo  5828  cbvexfo  5829  brabvv  5964  ov6g  6056  ectocld  6655  ecoptocl  6676  phplem3  6910  f1dmvrnfibi  7003  f1vrnfibi  7004  updjud  7141  pr2ne  7252  nn0ind-raph  9434  nn01to3  9682  modqmuladd  10437  modqmuladdnn0  10439  fihashf1rn  10859  hashfzp1  10895  rennim  11146  xrmaxiflemcom  11392  m1expe  12040  m1expo  12041  m1exp1  12042  nn0o1gt2  12046  flodddiv4  12075  cncongr1  12241  m1dvdsndvds  12386  mgmsscl  12944  mndinvmod  13026  ringinvnzdiv  13546  txcn  14443  relogbcxpbap  15097  logbgcd1irr  15099  logbgcd1irraplemexp  15100  zabsle1  15115  2lgsoddprmlem3  15199  bj-inf2vnlem2  15463