Theorem eqcoms 2741

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

Syntax hints:   → wi 4   = wceq 1541

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2725

This theorem is referenced by:  gencbvex  3496  sbceq2a  3749  eqimss2  3990  uneqdifeq  4442  tppreq3  4711  ifpprsnss  4716  tpprceq3  4755  preqsnd  4810  prproe  4856  copsex2t  5435  snopeqop  5449  opthhausdorff0  5461  optocl  5713  relopabi  5766  cnvimassrndm  6104  cnveqb  6148  cnveq0  6149  unixpid  6236  reuop  6245  f0rn0  6713  fimadmfo  6749  f1ssf1  6800  tz6.12i  6854  fveqdmss  7017  fvcofneq  7032  funopsn  7087  f1ocnvfv  7218  f1ocnvfvb  7219  cbvfo  7229  riotaeqimp  7335  ov6g  7516  tfindsg  7797  findsg  7833  mptcnfimad  7924  suppimacnv  8110  ectocld  8712  ecoptocl  8737  undifixp  8864  f1dmvrnfibi  9232  f1vrnfibi  9233  updjud  9834  card1  9868  prdom2  9904  sornom  10175  indpi  10805  ltlen  11221  eqlei  11230  squeeze0  12032  nn0ind-raph  12579  fzoopth  13664  injresinjlem  13692  fvf1tp  13695  modmuladd  13822  modmuladdnn0  13824  hashf1rn  14261  hashrabsn1  14283  hash1snb  14328  hashgt12el  14331  hashgt12el2  14332  hashfzp1  14340  hash2prde  14379  hash2pwpr  14385  fi1uzind  14416  brfi1indALT  14419  lswlgt0cl  14478  wrd2ind  14632  pfxccatin12lem2  14640  pfxccatin12lem3  14641  cshweqrep  14730  scshwfzeqfzo  14735  cshimadifsn  14738  cshimadifsn0  14739  2swrd2eqwrdeq  14862  wwlktovfo  14867  rennim  15148  absmod0  15212  modfsummods  15702  mod2eq1n2dvds  16260  m1expe  16287  m1expo  16288  m1exp1  16289  nn0o1gt2  16294  flodddiv4  16328  cncongr1  16580  ge2nprmge4  16614  m1dvdsndvds  16712  cshwrepswhash1  17016  initoeu2lem1  17923  istos  18324  mgmsscl  18555  mndinvmod  18674  smndex1n0mnd  18822  symgfvne  19295  symgfix2  19330  symgextf1  19335  symgfixelsi  19349  psgnsn  19434  odbezout  19472  cntzcmnss  19755  frgpnabllem1  19787  ringinvnzdiv  20221  rngcinv  20554  psgndiflemB  21539  uvcendim  21786  mamufacex  22312  smatvscl  22440  mavmulsolcl  22467  mdetunilem8  22535  pm2mpfo  22730  chpscmat  22758  chmaidscmat  22764  chfacfscmulgsum  22776  chfacfpmmulgsum  22780  txcn  23542  qtopeu  23632  reeff1o  26385  relogbcxpb  26725  logbgcd1irr  26732  fsumdvdsmul  27133  zabsle1  27235  2lgslem1c  27332  2lgsoddprmlem3  27353  2sq2  27372  2sqreultlem  27386  2sqreunnltlem  27389  2sqreulem3  27392  pntrlog2bndlem5  27520  sltlend  27711  upgrpredgv  29119  usgredg2vlem2  29206  ushgredgedg  29209  ushgredgedgloop  29211  uhgrspan1  29283  nb3grprlem1  29360  uvtxnbgrb  29381  cusgrsize2inds  29434  1egrvtxdg0  29492  uspgrloopvtxel  29497  finsumvtxdg2size  29531  rusgrpropnb  29564  ifpsnprss  29603  upgrwlkvtxedg  29625  uspgr2wlkeq  29626  wlkp1lem5  29656  wlkp1  29660  usgr2pth  29744  uspgrn2crct  29788  iswwlksnon  29833  wlkiswwlks1  29847  wlkiswwlks2lem3  29851  wwlksnextbi  29874  wwlksnredwwlkn0  29876  wwlksnextwrd  29877  wwlksnextsurj  29880  wwlksnextprop  29892  wspn0  29904  umgr2adedgwlkonALT  29927  umgr2adedgspth  29928  umgr2wlkon  29930  elwwlks2ons3  29935  elwwlks2on  29941  clwlkclwwlklem2a4  29979  clwlkclwwlklem2a  29980  clwlkclwwlkf1lem3  29988  clwwlkfo  30032  eleclclwwlknlem2  30043  erclwwlkntr  30053  hashecclwwlkn1  30059  umgrhashecclwwlk  30060  0wlkonlem1  30100  upgr1wlkdlem1  30127  1pthon2v  30135  upgr3v3e3cycl  30162  uhgr3cyclexlem  30163  upgr4cycl4dv4e  30167  eupth2lem3lem3  30212  eupth2lem3lem4  30213  1to2vfriswmgr  30261  frgrncvvdeqlem6  30286  frgrncvvdeqlem8  30288  frgrncvvdeqlem9  30289  frgrwopreglem2  30295  2clwwlk2clwwlk  30332  extwwlkfab  30334  numclwwlk1lem2f1  30339  numclwwlkovh  30355  numclwwlk2lem1  30358  numclwlk2lem2f  30359  cdj1i  32415  brabgaf  32591  br8d  32593  sgn3da  32822  onvf1odlem1  35168  spthcycl  35194  goalrlem  35461  goalr  35462  fmlasucdisj  35464  satffunlem  35466  satffunlem1lem1  35467  satffunlem1lem2  35468  satffunlem2lem1  35469  satffunlem2lem2  35471  mthmb  35646  br8  35821  br4  35823  bj-snsetex  37028  bj-snglc  37034  copsex2d  37204  poimirlem20  37700  poimirlem26  37706  poimirlem27  37707  mblfinlem3  37719  mblfinlem4  37720  itg2addnclem  37731  indexdom  37794  ismgmOLD  37910  rngodm1dm2  37992  rngomndo  37995  rngoueqz  38000  zerdivemp1x  38007  opcon3b  39315  ps-1  39596  3atlem5  39606  4atex  40195  selvvvval  42703  prjspvs  42728  iscard4  43650  pr2cv  43665  pm13.192  44527  iotavalsb  44550  relpfrlem  45070  fourierdlem32  46261  fourierdlem49  46277  fourierdlem64  46292  elprneb  47153  fveqvfvv  47164  funressnfv  47167  f1cof1b  47201  nvelim  47247  afvpcfv0  47270  afv0nbfvbi  47275  fnbrafvb  47278  tz6.12-afv  47297  afvco2  47300  ndmaovg  47308  afv2orxorb  47352  tz6.12-afv2  47364  tz6.12i-afv2  47367  f1oresf1o2  47415  elsetpreimafvbi  47515  imasetpreimafvbijlemfo  47529  iccpartiltu  47546  fargshiftfv  47563  fargshiftf  47564  lswn0  47568  prsprel  47611  reupr  47646  2exopprim  47649  fmtnorec2lem  47666  2pwp1prm  47713  lighneallem2  47730  lighneallem3  47731  proththd  47738  nn0o1gt2ALTV  47818  evenltle  47841  sbgoldbwt  47901  nnsum4primeseven  47924  nnsum4primesevenALTV  47925  clnbgrval  47946  dfvopnbgr2  47977  uhgrimedgi  48014  gricushgr  48041  clnbgrgrim  48058  grimedg  48059  cycl3grtri  48071  isubgr3stgrlem4  48093  uspgrlimlem1  48112  grlimgrtri  48127  gpgedg2ov  48190  gpgedg2iv  48191  pgnbgreunbgrlem1  48237  pgnbgreunbgrlem2lem3  48240  pgnbgreunbgrlem2  48241  pgnbgreunbgrlem4  48243  uspgropssxp  48268  lmod0rng  48353  lidldomn1  48355  zlidlring  48358  rngcinvALTV  48400  ztprmneprm  48471  lincext3  48581  zlmodzxznm  48622  suppdm  48635  elfzolborelfzop1  48644  nn0sumshdiglemB  48745  itcovalsucov  48793  lines  48856  rrx2vlinest  48866  line2xlem  48878  itschlc0yqe  48885  itsclquadeu  48902