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  9763  nn01to3  10017  modqmuladd  10803  modqmuladdnn0  10805  fihashf1rn  11227  hashfzp1  11265  lswlgt0cl  11357  wrd2ind  11495  pfxccatin12lem2  11503  pfxccatin12lem3  11504  rennim  11768  xrmaxiflemcom  12015  m1expe  12666  m1expo  12667  m1exp1  12668  nn0o1gt2  12672  flodddiv4  12703  cncongr1  12881  m1dvdsndvds  13027  mgmsscl  13681  mndinvmod  13758  ringinvnzdiv  14355  txcn  15376  relogbcxpbap  16067  logbgcd1irr  16069  logbgcd1irraplemexp  16070  fsumdvdsmul  16105  zabsle1  16118  2lgslem1c  16209  2lgsoddprmlem3  16230  upgrpredgv  16387  usgredg2vlem2  16464  ushgredgedg  16467  ushgredgedgloop  16469  ifpsnprss  16584  upgrwlkvtxedg  16605  uspgr2wlkeq  16606  eupth2lem3lem3fi  16711  eupth2lem3lem4fi  16714  bj-inf2vnlem2  16997