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  4385  copsex2g  4386  ordsoexmid  4709  0elsucexmid  4712  ordpwsucexmid  4717  cnveqb  5243  cnveq0  5244  relcoi1  5319  funtpg  5432  f0rn0  5587  fimadmfo  5624  f1ssf1  5671  f1ocnvfv  5985  f1ocnvfvb  5986  cbvfo  5991  cbvexfo  5992  riotaeqimp  6063  brabvv  6134  ov6g  6227  ectocld  6875  ecoptocl  6896  phplem3  7155  f1dmvrnfibi  7258  f1vrnfibi  7259  updjud  7422  pr2ne  7538  nn0ind-raph  9767  nn01to3  10026  modqmuladd  10816  modqmuladdnn0  10818  fihashf1rn  11241  hashfzp1  11279  lswlgt0cl  11371  wrd2ind  11509  pfxccatin12lem2  11517  pfxccatin12lem3  11518  rennim  11782  xrmaxiflemcom  12031  m1expe  12682  m1expo  12683  m1exp1  12684  nn0o1gt2  12688  flodddiv4  12719  cncongr1  12897  m1dvdsndvds  13047  mgmsscl  13730  mndinvmod  13807  ringinvnzdiv  14404  txcn  15425  relogbcxpbap  16120  logbgcd1irr  16122  logbgcd1irraplemexp  16123  fsumdvdsmul  16186  zabsle1  16216  2lgslem1c  16307  2lgsoddprmlem3  16328  upgrpredgv  16485  usgredg2vlem2  16562  ushgredgedg  16565  ushgredgedgloop  16567  ifpsnprss  16682  upgrwlkvtxedg  16703  uspgr2wlkeq  16704  eupth2lem3lem3fi  16809  eupth2lem3lem4fi  16812  bj-inf2vnlem2  17095