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 )

Syntax hints:   -> wi 4   = wceq 1402

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 1500  ax-gen 1502  ax-ext 2220

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

This theorem is referenced by:  gencbvex  2869  gencbval  2871  sbceq2a  3062  eqimss2  3303  uneqdifeqim  3610  tppreq3  3810  ifpprsnssdc  3815  copsex2t  4380  copsex2g  4381  ordsoexmid  4704  0elsucexmid  4707  ordpwsucexmid  4712  cnveqb  5238  cnveq0  5239  relcoi1  5314  funtpg  5427  f0rn0  5582  fimadmfo  5619  f1ssf1  5666  f1ocnvfv  5975  f1ocnvfvb  5976  cbvfo  5981  cbvexfo  5982  riotaeqimp  6053  brabvv  6124  ov6g  6217  ectocld  6865  ecoptocl  6886  phplem3  7145  f1dmvrnfibi  7248  f1vrnfibi  7249  updjud  7412  pr2ne  7528  nn0ind-raph  9742  nn01to3  9996  modqmuladd  10781  modqmuladdnn0  10783  fihashf1rn  11205  hashfzp1  11243  lswlgt0cl  11335  wrd2ind  11473  pfxccatin12lem2  11481  pfxccatin12lem3  11482  rennim  11746  xrmaxiflemcom  11993  m1expe  12644  m1expo  12645  m1exp1  12646  nn0o1gt2  12650  flodddiv4  12681  cncongr1  12859  m1dvdsndvds  13005  mgmsscl  13658  mndinvmod  13735  ringinvnzdiv  14328  txcn  15299  relogbcxpbap  15990  logbgcd1irr  15992  logbgcd1irraplemexp  15993  fsumdvdsmul  16019  zabsle1  16032  2lgslem1c  16123  2lgsoddprmlem3  16144  upgrpredgv  16301  usgredg2vlem2  16378  ushgredgedg  16381  ushgredgedgloop  16383  ifpsnprss  16498  upgrwlkvtxedg  16519  uspgr2wlkeq  16520  eupth2lem3lem3fi  16625  eupth2lem3lem4fi  16628  bj-inf2vnlem2  16911