Theorem eqcoms 2241

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 2240	. 2 |- ( B = A <-> A = B )
2		eqcoms.1	. 2 |- ( A = B -> ph )
3	1, 2	sylbi 121	1 |- ( B = A -> ph )

This proof depends on syntax axioms:   -> wi 4   = wceq 1402

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-cleq 2231

This theorem is used by:  gencbvex  2869  gencbval  2871  sbceq2a  3062  eqimss2  3303  uneqdifeqim  3613  tppreq3  3814  ifpprsnssdc  3820  copsex2t  4387  copsex2g  4388  ordsoexmid  4711  0elsucexmid  4714  ordpwsucexmid  4719  cnveqb  5246  cnveq0  5247  relcoi1  5322  funtpg  5435  f0rn0  5590  fimadmfo  5627  f1ssf1  5674  f1ocnvfv  5988  f1ocnvfvb  5989  cbvfo  5994  cbvexfo  5995  riotaeqimp  6066  brabvv  6137  ov6g  6230  ectocld  6880  ecoptocl  6901  phplem3  7161  f1dmvrnfibi  7264  f1vrnfibi  7265  updjud  7428  pr2ne  7544  nn0ind-raph  9773  nn01to3  10032  modqmuladd  10823  modqmuladdnn0  10825  fihashf1rn  11248  hashfzp1  11286  lswlgt0cl  11378  wrd2ind  11516  pfxccatin12lem2  11524  pfxccatin12lem3  11525  rennim  11789  xrmaxiflemcom  12039  m1expe  12690  m1expo  12691  m1exp1  12692  nn0o1gt2  12696  flodddiv4  12727  cncongr1  12905  m1dvdsndvds  13055  mgmsscl  13739  mndinvmod  13816  ringinvnzdiv  14461  txcn  15518  relogbcxpbap  16218  logbgcd1irr  16220  logbgcd1irraplemexp  16221  fsumdvdsmul  16302  zabsle1  16340  2lgslem1c  16431  2lgsoddprmlem3  16452  upgrpredgv  16609  usgredg2vlem2  16686  ushgredgedg  16689  ushgredgedgloop  16691  ifpsnprss  16806  upgrwlkvtxedg  16827  uspgr2wlkeq  16828  eupth2lem3lem3fi  16933  eupth2lem3lem4fi  16936  bj-inf2vnlem2  17219