Theorem eqcoms 2745

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 2744	. 2 ⊢ (𝐵 = 𝐴 ↔ 𝐴 = 𝐵)
2		eqcoms.1	. 2 ⊢ (𝐴 = 𝐵 → 𝜑)
3	1, 2	sylbi 217	1 ⊢ (𝐵 = 𝐴 → 𝜑)

Syntax hints:   → wi 4   = wceq 1542

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729

This theorem is referenced by:  gencbvex  3501  sbceq2a  3754  eqimss2  3995  uneqdifeq  4447  tppreq3  4718  ifpprsnss  4723  tpprceq3  4762  preqsnd  4817  prproe  4863  copsex2t  5448  snopeqop  5462  opthhausdorff0  5474  optocl  5726  relopabi  5779  cnvimassrndm  6118  cnveqb  6162  cnveq0  6163  unixpid  6250  reuop  6259  f0rn0  6727  fimadmfo  6763  f1ssf1  6814  tz6.12i  6868  fveqdmss  7032  fvcofneq  7047  funopsn  7103  f1ocnvfv  7234  f1ocnvfvb  7235  cbvfo  7245  riotaeqimp  7351  ov6g  7532  tfindsg  7813  findsg  7849  mptcnfimad  7940  suppimacnv  8126  ectocld  8731  ecoptocl  8756  undifixp  8884  f1dmvrnfibi  9253  f1vrnfibi  9254  updjud  9858  card1  9892  prdom2  9928  sornom  10199  indpi  10830  ltlen  11246  eqlei  11255  squeeze0  12057  nn0ind-raph  12604  fzoopth  13690  injresinjlem  13718  fvf1tp  13721  modmuladd  13848  modmuladdnn0  13850  hashf1rn  14287  hashrabsn1  14309  hash1snb  14354  hashgt12el  14357  hashgt12el2  14358  hashfzp1  14366  hash2prde  14405  hash2pwpr  14411  fi1uzind  14442  brfi1indALT  14445  lswlgt0cl  14504  wrd2ind  14658  pfxccatin12lem2  14666  pfxccatin12lem3  14667  cshweqrep  14756  scshwfzeqfzo  14761  cshimadifsn  14764  cshimadifsn0  14765  2swrd2eqwrdeq  14888  wwlktovfo  14893  rennim  15174  absmod0  15238  modfsummods  15728  mod2eq1n2dvds  16286  m1expe  16313  m1expo  16314  m1exp1  16315  nn0o1gt2  16320  flodddiv4  16354  cncongr1  16606  ge2nprmge4  16640  m1dvdsndvds  16738  cshwrepswhash1  17042  initoeu2lem1  17950  istos  18351  mgmsscl  18582  mndinvmod  18701  smndex1n0mnd  18849  symgfvne  19322  symgfix2  19357  symgextf1  19362  symgfixelsi  19376  psgnsn  19461  odbezout  19499  cntzcmnss  19782  frgpnabllem1  19814  ringinvnzdiv  20248  rngcinv  20582  psgndiflemB  21567  uvcendim  21814  mamufacex  22352  smatvscl  22480  mavmulsolcl  22507  mdetunilem8  22575  pm2mpfo  22770  chpscmat  22798  chmaidscmat  22804  chfacfscmulgsum  22816  chfacfpmmulgsum  22820  txcn  23582  qtopeu  23672  reeff1o  26425  relogbcxpb  26765  logbgcd1irr  26772  fsumdvdsmul  27173  zabsle1  27275  2lgslem1c  27372  2lgsoddprmlem3  27393  2sq2  27412  2sqreultlem  27426  2sqreunnltlem  27429  2sqreulem3  27432  pntrlog2bndlem5  27560  ltlesnd  27755  upgrpredgv  29224  usgredg2vlem2  29311  ushgredgedg  29314  ushgredgedgloop  29316  uhgrspan1  29388  nb3grprlem1  29465  uvtxnbgrb  29486  cusgrsize2inds  29539  1egrvtxdg0  29597  uspgrloopvtxel  29602  finsumvtxdg2size  29636  rusgrpropnb  29669  ifpsnprss  29708  upgrwlkvtxedg  29730  uspgr2wlkeq  29731  wlkp1lem5  29761  wlkp1  29765  usgr2pth  29849  uspgrn2crct  29893  iswwlksnon  29938  wlkiswwlks1  29952  wlkiswwlks2lem3  29956  wwlksnextbi  29979  wwlksnredwwlkn0  29981  wwlksnextwrd  29982  wwlksnextsurj  29985  wwlksnextprop  29997  wspn0  30009  umgr2adedgwlkonALT  30032  umgr2adedgspth  30033  umgr2wlkon  30035  elwwlks2ons3  30040  elwwlks2on  30046  clwlkclwwlklem2a4  30084  clwlkclwwlklem2a  30085  clwlkclwwlkf1lem3  30093  clwwlkfo  30137  eleclclwwlknlem2  30148  erclwwlkntr  30158  hashecclwwlkn1  30164  umgrhashecclwwlk  30165  0wlkonlem1  30205  upgr1wlkdlem1  30232  1pthon2v  30240  upgr3v3e3cycl  30267  uhgr3cyclexlem  30268  upgr4cycl4dv4e  30272  eupth2lem3lem3  30317  eupth2lem3lem4  30318  1to2vfriswmgr  30366  frgrncvvdeqlem6  30391  frgrncvvdeqlem8  30393  frgrncvvdeqlem9  30394  frgrwopreglem2  30400  2clwwlk2clwwlk  30437  extwwlkfab  30439  numclwwlk1lem2f1  30444  numclwwlkovh  30460  numclwwlk2lem1  30463  numclwlk2lem2f  30464  cdj1i  32520  brabgaf  32695  br8d  32697  sgn3da  32925  onvf1odlem1  35316  spthcycl  35342  goalrlem  35609  goalr  35610  fmlasucdisj  35612  satffunlem  35614  satffunlem1lem1  35615  satffunlem1lem2  35616  satffunlem2lem1  35617  satffunlem2lem2  35619  mthmb  35794  br8  35969  br4  35971  bj-snsetex  37205  bj-snglc  37211  copsex2d  37388  poimirlem20  37885  poimirlem26  37891  poimirlem27  37892  mblfinlem3  37904  mblfinlem4  37905  itg2addnclem  37916  indexdom  37979  ismgmOLD  38095  rngodm1dm2  38177  rngomndo  38180  rngoueqz  38185  zerdivemp1x  38192  opcon3b  39566  ps-1  39847  3atlem5  39857  4atex  40446  selvvvval  42937  prjspvs  42962  iscard4  43883  pr2cv  43898  pm13.192  44760  iotavalsb  44783  relpfrlem  45303  fourierdlem32  46491  fourierdlem49  46507  fourierdlem64  46522  elprneb  47383  fveqvfvv  47394  funressnfv  47397  f1cof1b  47431  nvelim  47477  afvpcfv0  47500  afv0nbfvbi  47505  fnbrafvb  47508  tz6.12-afv  47527  afvco2  47530  ndmaovg  47538  afv2orxorb  47582  tz6.12-afv2  47594  tz6.12i-afv2  47597  f1oresf1o2  47645  elsetpreimafvbi  47745  imasetpreimafvbijlemfo  47759  iccpartiltu  47776  fargshiftfv  47793  fargshiftf  47794  lswn0  47798  prsprel  47841  reupr  47876  2exopprim  47879  fmtnorec2lem  47896  2pwp1prm  47943  lighneallem2  47960  lighneallem3  47961  proththd  47968  nn0o1gt2ALTV  48048  evenltle  48071  sbgoldbwt  48131  nnsum4primeseven  48154  nnsum4primesevenALTV  48155  clnbgrval  48176  dfvopnbgr2  48207  uhgrimedgi  48244  gricushgr  48271  clnbgrgrim  48288  grimedg  48289  cycl3grtri  48301  isubgr3stgrlem4  48323  uspgrlimlem1  48342  grlimgrtri  48357  gpgedg2ov  48420  gpgedg2iv  48421  pgnbgreunbgrlem1  48467  pgnbgreunbgrlem2lem3  48470  pgnbgreunbgrlem2  48471  pgnbgreunbgrlem4  48473  uspgropssxp  48498  lmod0rng  48583  lidldomn1  48585  zlidlring  48588  rngcinvALTV  48630  ztprmneprm  48701  lincext3  48810  zlmodzxznm  48851  suppdm  48864  elfzolborelfzop1  48873  nn0sumshdiglemB  48974  itcovalsucov  49022  lines  49085  rrx2vlinest  49095  line2xlem  49107  itschlc0yqe  49114  itsclquadeu  49131