Theorem eqcoms 2618

Description: Inference applying commutative law for class equality to an antecedent. (Contributed by NM, 24-Jun-1993.)

Hypothesis

Ref	Expression
eqcoms.1	⊢ (𝐴 = 𝐵 → 𝜑)

Assertion

Ref	Expression
eqcoms	⊢ (𝐵 = 𝐴 → 𝜑)

Proof of Theorem eqcoms

Step	Hyp	Ref	Expression
1		eqcom 2617	. 2 ⊢ (𝐵 = 𝐴 ↔ 𝐴 = 𝐵)
2		eqcoms.1	. 2 ⊢ (𝐴 = 𝐵 → 𝜑)
3	1, 2	sylbi 206	1 ⊢ (𝐵 = 𝐴 → 𝜑)

Syntax hints:   → wi 4   = wceq 1475

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-cleq 2603

This theorem is referenced by:  gencbvex  3223  sbceq2a  3414  eqimss2  3621  uneqdifeq  4009  uneqdifeqOLD  4010  tppreq3  4238  tpprceq3  4276  elpr2elpr  4336  copsex2t  4883  copsex2g  4884  relopabi  5167  cnveqb  5508  cnveq0  5509  unixpid  5587  funtpgOLD  5857  f0rn0  6003  tz6.12i  6124  fveqdmss  6262  fvcofneq  6275  funopsn  6319  f1ocnvfv  6434  f1ocnvfvb  6435  cbvfo  6444  ov6g  6696  tfindsg  6952  findsg  6985  suppimacnv  7193  suppss  7212  ectocld  7701  ecoptocl  7724  undifixp  7830  phplem3  8026  f1dmvrnfibi  8133  f1vrnfibi  8134  card1  8677  pr2ne  8711  prdom2  8712  sornom  8982  indpi  9608  ltlen  10017  eqlei  10026  squeeze0  10805  nn0ind-raph  11353  injresinjlem  12450  modmuladd  12574  modmuladdnn0  12576  hashf1rn  13004  hashf1rnOLD  13005  hashrabsn1  13024  hash1snb  13068  hashgt12el  13070  hashgt12el2  13071  hashfzp1  13078  hash2prde  13109  hash2pwpr  13115  fi1uzind  13134  brfi1indALT  13137  fi1uzindOLD  13140  brfi1indALTOLD  13143  lswlgt0cl  13209  wrd2ind  13329  reuccats1lem  13331  swrdccatin12lem2  13340  swrdccatin12lem3  13341  swrdccat3a  13345  cshweqrep  13418  cshwsexa  13421  scshwfzeqfzo  13423  cshimadifsn  13426  cshimadifsn0  13427  2swrd2eqwrdeq  13544  wwlktovfo  13549  rennim  13827  absmod0  13891  modfsummods  14366  mod2eq1n2dvds  14909  m1expe  14929  m1expo  14930  m1exp1  14931  nn0o1gt2  14935  flodddiv4  14975  cncongr1  15219  m1dvdsndvds  15341  cshwrepswhash1  15647  xpsfrnel2  16048  initoeu2lem1  16487  istos  16858  symgfvne  17631  symgfix2  17659  symgextf1  17664  symgfixelsi  17678  psgnsn  17763  odbezout  17798  cntzcmnss  18069  frgpnabllem1  18099  ringinvnzdiv  18416  psgndiflemB  19765  uvcendim  20005  mamufacex  20014  smatvscl  20149  mavmulsolcl  20176  mdetunilem8  20244  pm2mpfo  20438  chpscmat  20466  chmaidscmat  20472  chfacfscmulgsum  20484  chfacfpmmulgsum  20488  txcn  21239  qtopeu  21329  reeff1o  24005  relogbcxpb  24325  zabsle1  24821  2lgslem1c  24918  2lgsoddprmlem3  24939  pntrlog2bndlem5  25070  usgraedg4  25916  usgraidx2vlem2  25921  nbgraf1olem5  25974  nb3graprlem1  25980  cusgrasize2inds  26005  usgrasscusgra  26011  wlkn0  26055  2pthlem2  26126  wlkdvspthlem  26137  usgra2wlkspthlem1  26147  fargshiftfv  26163  fargshiftf  26164  usgrcyclnl1  26168  usgrcyclnl2  26169  3v3e3cycl1  26172  constr3trllem2  26179  4cycl4v4e  26194  4cycl4dv4e  26196  wwlkn0  26217  wlkiswwlk1  26218  wlkiswwlk2lem3  26221  wlklniswwlkn1  26227  usg2wlkeq  26236  wwlknextbi  26253  wwlknredwwlkn0  26255  wwlkextwrd  26256  wwlkextsur  26259  wwlkextprop  26272  clwlkisclwwlklem2a4  26312  clwlkisclwwlklem2a  26313  clwwlkel  26321  clwwlkfo  26325  wwlkext2clwwlk  26331  clwwnisshclwwn  26337  eleclclwwlknlem2  26346  erclwwlkneqlen  26352  erclwwlkntr  26355  hashecclwwlkn1  26361  usghashecclwwlk  26362  clwlkfclwwlk  26371  clwlkfoclwwlk  26372  el2wlkonot  26396  el2spthonot  26397  el2spthonot0  26398  el2wlkonotot0  26399  el2wlkonotot1  26401  usg2spthonot0  26416  vdusgra0nedg  26435  usgravd0nedg  26445  rusgraprop2  26469  clwlknclwlkdifs  26487  eupatrl  26495  1to2vfriswmgra  26533  frgrancvvdeqlem3  26559  frgrancvvdeqlem4  26560  frgrancvvdeqlemB  26565  frgrancvvdeqlemC  26566  usgreghash2spotv  26593  extwwlkfablem1  26601  extwwlkfablem2  26605  numclwlk1lem2f1  26621  numclwwlk2lem1  26629  numclwlk2lem2f  26630  cdj1i  28676  brabgaf  28800  br8d  28802  sgn3da  29930  mthmb  30732  br8  30899  br4  30901  bj-snsetex  32144  bj-snglc  32150  poimirlem20  32599  poimirlem26  32605  poimirlem27  32606  mblfinlem3  32618  mblfinlem4  32619  itg2addnclem  32631  indexdom  32699  ismgmOLD  32819  rngodm1dm2  32901  rngomndo  32904  rngoueqz  32909  zerdivemp1x  32916  opcon3b  33501  ps-1  33781  3atlem5  33791  4atex  34380  pm13.192  37633  iotavalsb  37656  fourierdlem32  39032  fourierdlem49  39048  fourierdlem64  39063  nvelim  39849  fveqvfvv  39853  funressnfv  39857  afvpcfv0  39875  afv0nbfvbi  39880  fnbrafvb  39883  tz6.12-afv  39902  afvco2  39905  ndmaovg  39913  elprneb  39939  iccpartiltu  39960  fmtnorec2lem  39992  2pwp1prm  40041  lighneallem2  40061  lighneallem3  40062  proththd  40069  nn0o1gt2ALTV  40143  bgoldbwt  40199  nnsum4primeseven  40216  nnsum4primesevenALTV  40217  lswn0  40242  pfxsuffeqwrdeq  40269  pfxccatin12lem2  40287  f1ssf1  40328  riotaeqimp  40338  fzoopth  40360  usgredg2vlem2  40453  ushgredgedga  40456  ushgredgedgaloop  40458  uhgrspan1  40527  nb3grprlem1  40608  uvtxnbgrb  40628  cplgruvtxb  40637  cusgrsize2inds  40669  1egrvtxdg0  40727  uspgrloopvtxel  40732  rusgrpropnb  40783  1wlkvtxeledglem  40827  ifpprsnss  40845  upgr1wlkvtxedg  40853  uspgr2wlkeq  40854  1wlkp1lem5  40886  1wlkp1  40890  usgr2pth  40970  uspgrn2crct  41011  1wlkiswwlks1  41064  1wlkiswwlks2lem3  41068  wwlksnextbi  41100  wwlksnredwwlkn0  41102  wwlksnextwrd  41103  wwlksnextsur  41106  wwlksnextprop  41118  wspn0  41131  umgr2adedgwlkonALT  41154  umgr2adedgspth  41155  umgr2wlkon  41157  elwwlks2ons3  41159  elwwlks2on  41162  clwwlknclwwlkdifs  41181  isclwwlksng  41196  isclwwlksnx  41197  clwlkclwwlklem2a4  41206  clwlkclwwlklem2a  41207  clwwlksel  41221  clwwlksfo  41225  wwlksext2clwwlk  41231  clwwnisshclwwsn  41237  eleclclwwlksnlem2  41246  erclwwlksntr  41255  hashecclwwlksn1  41261  umgrhashecclwwlk  41262  clwlksfclwwlk  41269  clwlksfoclwwlk  41270  0wlkOnlem1  41286  upgr11wlkdlem1  41312  1pthon2v-av  41320  upgr3v3e3cycl  41347  uhgr3cyclexlem  41348  upgr4cycl4dv4e  41352  eupth2lem3lem3  41398  eupth2lem3lem4  41399  1to2vfriswmgr  41449  frgrncvvdeqlem3  41471  frgrncvvdeqlem4  41472  frgrncvvdeqlemB  41477  frgrncvvdeqlemC  41478  fusgreghash2wspv  41499  av-extwwlkfablem1  41508  av-extwwlkfab  41520  av-numclwlk1lem2f1  41524  av-numclwwlk2lem1  41532  av-numclwlk2lem2f  41533  lmod0rng  41658  lidldomn1  41711  zlidlring  41718  rngcinv  41773  rngcinvALTV  41785  ringcinv  41824  ringcinvALTV  41848  ztprmneprm  41918  lincext3  42039  zlmodzxznm  42080  suppdm  42094  elfzolborelfzop1  42103  nn0sumshdiglemB  42212