Theorem eqcoms 2630

Description: Inference applying commutative law for class equality to an antecedent. (Contributed by NM, 24-Jun-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 2629	. 2 |- ( B = A <-> A = B )
2		eqcoms.1	. 2 |- ( A = B -> ph )
3	1, 2	sylbi 207	1 |- ( B = A -> ph )

Syntax hints:   -> wi 4   = wceq 1483

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-cleq 2615

This theorem is referenced by:  gencbvex  3250  sbceq2a  3447  eqimss2  3658  uneqdifeq  4057  uneqdifeqOLD  4058  tppreq3  4294  ifpprsnss  4299  tpprceq3  4335  elpr2elpr  4398  prproe  4434  copsex2t  4957  copsex2g  4958  relopabi  5245  cnveqb  5590  cnveq0  5591  unixpid  5670  funtpgOLD  5943  f0rn0  6090  f1ssf1  6168  tz6.12i  6214  fveqdmss  6354  fvcofneq  6367  funopsn  6413  f1ocnvfv  6534  f1ocnvfvb  6535  cbvfo  6544  riotaeqimp  6634  ov6g  6798  tfindsg  7060  findsg  7093  suppimacnv  7306  suppss  7325  ectocld  7814  ecoptocl  7837  undifixp  7944  phplem3  8141  f1dmvrnfibi  8250  f1vrnfibi  8251  card1  8794  pr2ne  8828  prdom2  8829  sornom  9099  indpi  9729  ltlen  10138  eqlei  10147  squeeze0  10926  nn0ind-raph  11477  injresinjlem  12588  modmuladd  12712  modmuladdnn0  12714  hashf1rn  13142  hashf1rnOLD  13143  hashrabsn1  13163  hash1snb  13207  hashgt12el  13210  hashgt12el2  13211  hashfzp1  13218  hash2prde  13252  hash2pwpr  13258  fi1uzind  13279  brfi1indALT  13282  fi1uzindOLD  13285  brfi1indALTOLD  13288  lswlgt0cl  13356  wrd2ind  13477  reuccats1lem  13479  swrdccatin12lem2  13489  swrdccatin12lem3  13490  swrdccat3a  13494  cshweqrep  13567  cshwsexa  13570  scshwfzeqfzo  13572  cshimadifsn  13575  cshimadifsn0  13576  2swrd2eqwrdeq  13696  wwlktovfo  13701  rennim  13979  absmod0  14043  modfsummods  14525  mod2eq1n2dvds  15071  m1expe  15091  m1expo  15092  m1exp1  15093  nn0o1gt2  15097  flodddiv4  15137  cncongr1  15381  m1dvdsndvds  15503  cshwrepswhash1  15809  xpsfrnel2  16225  initoeu2lem1  16664  istos  17035  symgfvne  17808  symgfix2  17836  symgextf1  17841  symgfixelsi  17855  psgnsn  17940  odbezout  17975  cntzcmnss  18246  frgpnabllem1  18276  ringinvnzdiv  18593  psgndiflemB  19946  uvcendim  20186  mamufacex  20195  smatvscl  20330  mavmulsolcl  20357  mdetunilem8  20425  pm2mpfo  20619  chpscmat  20647  chmaidscmat  20653  chfacfscmulgsum  20665  chfacfpmmulgsum  20669  txcn  21429  qtopeu  21519  reeff1o  24201  relogbcxpb  24525  zabsle1  25021  2lgslem1c  25118  2lgsoddprmlem3  25139  pntrlog2bndlem5  25270  upgrpredgv  26034  usgredg2vlem2  26118  ushgredgedg  26121  ushgredgedgloop  26123  uhgrspan1  26195  nb3grprlem1  26282  uvtxnbgrb  26302  cplgruvtxb  26311  cusgrsize2inds  26349  1egrvtxdg0  26407  uspgrloopvtxel  26412  finsumvtxdg2size  26446  rusgrpropnb  26479  ifpsnprss  26518  upgrwlkvtxedg  26541  uspgr2wlkeq  26542  wlkp1lem5  26574  wlkp1  26578  usgr2pth  26660  uspgrn2crct  26700  wlkiswwlks1  26753  wlkiswwlks2lem3  26757  wwlksnextbi  26789  wwlksnredwwlkn0  26791  wwlksnextwrd  26792  wwlksnextsur  26795  wwlksnextprop  26807  wspn0  26820  umgr2adedgwlkonALT  26843  umgr2adedgspth  26844  umgr2wlkon  26846  elwwlks2ons3  26848  elwwlks2on  26852  clwwlknclwwlkdifs  26873  isclwwlksng  26888  isclwwlksnx  26889  clwlkclwwlklem2a4  26898  clwlkclwwlklem2a  26899  clwwlksel  26914  clwwlksfo  26918  wwlksext2clwwlk  26924  clwwnisshclwwsn  26930  eleclclwwlksnlem2  26939  erclwwlksntr  26948  hashecclwwlksn1  26954  umgrhashecclwwlk  26955  clwlksfclwwlk  26962  clwlksfoclwwlk  26963  0wlkonlem1  26979  upgr1wlkdlem1  27005  1pthon2v  27013  upgr3v3e3cycl  27040  uhgr3cyclexlem  27041  upgr4cycl4dv4e  27045  eupth2lem3lem3  27090  eupth2lem3lem4  27091  1to2vfriswmgr  27143  frgrncvvdeqlem6  27168  frgrncvvdeqlem8  27170  frgrncvvdeqlem9  27171  frgrwopreglem2  27177  extwwlkfab  27223  numclwlk1lem2f1  27227  numclwwlk2lem1  27235  numclwlk2lem2f  27236  cdj1i  29292  brabgaf  29420  br8d  29422  sgn3da  30603  mthmb  31478  br8  31646  br4  31648  bj-snsetex  32951  bj-snglc  32957  poimirlem20  33429  poimirlem26  33435  poimirlem27  33436  mblfinlem3  33448  mblfinlem4  33449  itg2addnclem  33461  indexdom  33529  ismgmOLD  33649  rngodm1dm2  33731  rngomndo  33734  rngoueqz  33739  zerdivemp1x  33746  opcon3b  34483  ps-1  34763  3atlem5  34773  4atex  35362  pm13.192  38611  iotavalsb  38634  fourierdlem32  40356  fourierdlem49  40372  fourierdlem64  40387  nvelim  41200  fveqvfvv  41204  funressnfv  41208  afvpcfv0  41226  afv0nbfvbi  41231  fnbrafvb  41234  tz6.12-afv  41253  afvco2  41256  ndmaovg  41264  elprneb  41296  fzoopth  41337  iccpartiltu  41358  fargshiftfv  41375  fargshiftf  41376  lswn0  41380  pfxsuffeqwrdeq  41406  pfxccatin12lem2  41424  fmtnorec2lem  41454  2pwp1prm  41503  lighneallem2  41523  lighneallem3  41524  proththd  41531  nn0o1gt2ALTV  41605  evenltle  41626  sbgoldbwt  41665  nnsum4primeseven  41688  nnsum4primesevenALTV  41689  prsprel  41737  uspgropssxp  41752  lmod0rng  41868  lidldomn1  41921  zlidlring  41928  rngcinv  41981  rngcinvALTV  41993  ringcinv  42032  ringcinvALTV  42056  ztprmneprm  42125  lincext3  42245  zlmodzxznm  42286  suppdm  42300  elfzolborelfzop1  42309  nn0sumshdiglemB  42414