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  6879  ecoptocl  6900  phplem3  7159  f1dmvrnfibi  7262  f1vrnfibi  7263  updjud  7428  pr2ne  7544  nn0ind-raph  9774  nn01to3  10033  modqmuladd  10824  modqmuladdnn0  10826  fihashf1rn  11249  hashfzp1  11287  lswlgt0cl  11379  wrd2ind  11517  pfxccatin12lem2  11525  pfxccatin12lem3  11526  rennim  11790  xrmaxiflemcom  12040  m1expe  12691  m1expo  12692  m1exp1  12693  nn0o1gt2  12697  flodddiv4  12728  cncongr1  12906  m1dvdsndvds  13056  mgmsscl  13740  mndinvmod  13817  ringinvnzdiv  14462  txcn  15501  relogbcxpbap  16201  logbgcd1irr  16203  logbgcd1irraplemexp  16204  fsumdvdsmul  16285  zabsle1  16323  2lgslem1c  16414  2lgsoddprmlem3  16435  upgrpredgv  16592  usgredg2vlem2  16669  ushgredgedg  16672  ushgredgedgloop  16674  ifpsnprss  16789  upgrwlkvtxedg  16810  uspgr2wlkeq  16811  eupth2lem3lem3fi  16916  eupth2lem3lem4fi  16919  bj-inf2vnlem2  17202