Theorem eqcoms 2237

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 2236	. 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 1398

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 1496  ax-gen 1498  ax-ext 2216

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

This theorem is referenced by:  gencbvex  2863  gencbval  2865  sbceq2a  3056  eqimss2  3297  uneqdifeqim  3599  tppreq3  3799  ifpprsnssdc  3804  copsex2t  4366  copsex2g  4367  ordsoexmid  4689  0elsucexmid  4692  ordpwsucexmid  4697  cnveqb  5223  cnveq0  5224  relcoi1  5299  funtpg  5412  f0rn0  5567  fimadmfo  5604  f1ssf1  5651  f1ocnvfv  5958  f1ocnvfvb  5959  cbvfo  5964  cbvexfo  5965  riotaeqimp  6036  brabvv  6107  ov6g  6200  ectocld  6848  ecoptocl  6869  phplem3  7121  f1dmvrnfibi  7224  f1vrnfibi  7225  updjud  7386  pr2ne  7502  nn0ind-raph  9713  nn01to3  9967  modqmuladd  10752  modqmuladdnn0  10754  fihashf1rn  11176  hashfzp1  11214  lswlgt0cl  11302  wrd2ind  11440  pfxccatin12lem2  11448  pfxccatin12lem3  11449  rennim  11712  xrmaxiflemcom  11959  m1expe  12610  m1expo  12611  m1exp1  12612  nn0o1gt2  12616  flodddiv4  12647  cncongr1  12825  m1dvdsndvds  12971  mgmsscl  13624  mndinvmod  13706  ringinvnzdiv  14293  txcn  15266  relogbcxpbap  15956  logbgcd1irr  15958  logbgcd1irraplemexp  15959  fsumdvdsmul  15985  zabsle1  15998  2lgslem1c  16089  2lgsoddprmlem3  16110  upgrpredgv  16267  usgredg2vlem2  16344  ushgredgedg  16347  ushgredgedgloop  16349  ifpsnprss  16464  upgrwlkvtxedg  16485  uspgr2wlkeq  16486  eupth2lem3lem3fi  16591  eupth2lem3lem4fi  16594  bj-inf2vnlem2  16867