Theorem eqcoms 2742

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

Syntax hints:   → wi 4   = wceq 1536

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-cleq 2726

This theorem is referenced by:  gencbvex  3540  sbceq2a  3802  eqimss2  4054  uneqdifeq  4498  tppreq3  4763  ifpprsnss  4768  tpprceq3  4808  preqsnd  4863  prproe  4909  copsex2t  5502  snopeqop  5515  opthhausdorff0  5527  relopabi  5834  cnvimassrndm  6173  cnveqb  6217  cnveq0  6218  unixpid  6305  reuop  6314  f0rn0  6793  fimadmfo  6829  f1ssf1  6880  tz6.12i  6934  fveqdmss  7097  fvcofneq  7112  funopsn  7167  f1ocnvfv  7297  f1ocnvfvb  7298  cbvfo  7308  riotaeqimp  7413  ov6g  7596  tfindsg  7881  findsg  7919  mptcnfimad  8009  suppimacnv  8197  ectocld  8822  ecoptocl  8845  undifixp  8972  phplem3OLD  9253  f1dmvrnfibi  9378  f1vrnfibi  9379  updjud  9971  card1  10005  pr2neOLD  10042  prdom2  10043  sornom  10314  indpi  10944  ltlen  11359  eqlei  11368  squeeze0  12168  nn0ind-raph  12715  fzoopth  13797  injresinjlem  13822  fvf1tp  13825  modmuladd  13950  modmuladdnn0  13952  hashf1rn  14387  hashrabsn1  14409  hash1snb  14454  hashgt12el  14457  hashgt12el2  14458  hashfzp1  14466  hash2prde  14505  hash2pwpr  14511  fi1uzind  14542  brfi1indALT  14545  lswlgt0cl  14603  wrd2ind  14757  pfxccatin12lem2  14765  pfxccatin12lem3  14766  cshweqrep  14855  cshwsexaOLD  14859  scshwfzeqfzo  14861  cshimadifsn  14864  cshimadifsn0  14865  2swrd2eqwrdeq  14988  wwlktovfo  14993  rennim  15274  absmod0  15338  modfsummods  15825  mod2eq1n2dvds  16380  m1expe  16407  m1expo  16408  m1exp1  16409  nn0o1gt2  16414  flodddiv4  16448  cncongr1  16700  ge2nprmge4  16734  m1dvdsndvds  16831  cshwrepswhash1  17136  initoeu2lem1  18067  istos  18475  mgmsscl  18670  mndinvmod  18789  smndex1n0mnd  18937  symgfvne  19412  symgfix2  19448  symgextf1  19453  symgfixelsi  19467  psgnsn  19552  odbezout  19590  cntzcmnss  19873  frgpnabllem1  19905  ringinvnzdiv  20314  rngcinv  20653  psgndiflemB  21635  uvcendim  21884  mamufacex  22415  smatvscl  22545  mavmulsolcl  22572  mdetunilem8  22640  pm2mpfo  22835  chpscmat  22863  chmaidscmat  22869  chfacfscmulgsum  22881  chfacfpmmulgsum  22885  txcn  23649  qtopeu  23739  reeff1o  26505  relogbcxpb  26844  logbgcd1irr  26851  fsumdvdsmul  27252  zabsle1  27354  2lgslem1c  27451  2lgsoddprmlem3  27472  2sq2  27491  2sqreultlem  27505  2sqreunnltlem  27508  2sqreulem3  27511  pntrlog2bndlem5  27639  sltlend  27830  upgrpredgv  29170  usgredg2vlem2  29257  ushgredgedg  29260  ushgredgedgloop  29262  uhgrspan1  29334  nb3grprlem1  29411  uvtxnbgrb  29432  cusgrsize2inds  29485  1egrvtxdg0  29543  uspgrloopvtxel  29548  finsumvtxdg2size  29582  rusgrpropnb  29615  ifpsnprss  29655  upgrwlkvtxedg  29677  uspgr2wlkeq  29678  wlkp1lem5  29709  wlkp1  29713  usgr2pth  29796  uspgrn2crct  29837  iswwlksnon  29882  wlkiswwlks1  29896  wlkiswwlks2lem3  29900  wwlksnextbi  29923  wwlksnredwwlkn0  29925  wwlksnextwrd  29926  wwlksnextsurj  29929  wwlksnextprop  29941  wspn0  29953  umgr2adedgwlkonALT  29976  umgr2adedgspth  29977  umgr2wlkon  29979  elwwlks2ons3  29984  elwwlks2on  29988  clwlkclwwlklem2a4  30025  clwlkclwwlklem2a  30026  clwlkclwwlkf1lem3  30034  clwwlkfo  30078  eleclclwwlknlem2  30089  erclwwlkntr  30099  hashecclwwlkn1  30105  umgrhashecclwwlk  30106  0wlkonlem1  30146  upgr1wlkdlem1  30173  1pthon2v  30181  upgr3v3e3cycl  30208  uhgr3cyclexlem  30209  upgr4cycl4dv4e  30213  eupth2lem3lem3  30258  eupth2lem3lem4  30259  1to2vfriswmgr  30307  frgrncvvdeqlem6  30332  frgrncvvdeqlem8  30334  frgrncvvdeqlem9  30335  frgrwopreglem2  30341  2clwwlk2clwwlk  30378  extwwlkfab  30380  numclwwlk1lem2f1  30385  numclwwlkovh  30401  numclwwlk2lem1  30404  numclwlk2lem2f  30405  cdj1i  32461  brabgaf  32627  br8d  32629  sgn3da  34522  spthcycl  35113  goalrlem  35380  goalr  35381  fmlasucdisj  35383  satffunlem  35385  satffunlem1lem1  35386  satffunlem1lem2  35387  satffunlem2lem1  35388  satffunlem2lem2  35390  mthmb  35565  br8  35735  br4  35737  bj-snsetex  36945  bj-snglc  36951  copsex2d  37121  poimirlem20  37626  poimirlem26  37632  poimirlem27  37633  mblfinlem3  37645  mblfinlem4  37646  itg2addnclem  37657  indexdom  37720  ismgmOLD  37836  rngodm1dm2  37918  rngomndo  37921  rngoueqz  37926  zerdivemp1x  37933  opcon3b  39177  ps-1  39459  3atlem5  39469  4atex  40058  selvvvval  42571  prjspvs  42596  iscard4  43522  pr2cv  43537  pm13.192  44405  iotavalsb  44428  fourierdlem32  46094  fourierdlem49  46110  fourierdlem64  46125  elprneb  46978  fveqvfvv  46989  funressnfv  46992  f1cof1b  47026  nvelim  47072  afvpcfv0  47095  afv0nbfvbi  47100  fnbrafvb  47103  tz6.12-afv  47122  afvco2  47125  ndmaovg  47133  afv2orxorb  47177  tz6.12-afv2  47189  tz6.12i-afv2  47192  f1oresf1o2  47240  elsetpreimafvbi  47315  imasetpreimafvbijlemfo  47329  iccpartiltu  47346  fargshiftfv  47363  fargshiftf  47364  lswn0  47368  prsprel  47411  reupr  47446  2exopprim  47449  fmtnorec2lem  47466  2pwp1prm  47513  lighneallem2  47530  lighneallem3  47531  proththd  47538  nn0o1gt2ALTV  47618  evenltle  47641  sbgoldbwt  47701  nnsum4primeseven  47724  nnsum4primesevenALTV  47725  clnbgrval  47746  dfvopnbgr2  47776  gricushgr  47823  clnbgrgrim  47839  grimedg  47840  isubgr3stgrlem4  47871  uspgrlimlem1  47890  grlimgrtri  47898  uspgropssxp  47987  lmod0rng  48072  lidldomn1  48074  zlidlring  48077  rngcinvALTV  48119  ztprmneprm  48191  lincext3  48301  zlmodzxznm  48342  suppdm  48355  elfzolborelfzop1  48364  nn0sumshdiglemB  48469  itcovalsucov  48517  lines  48580  rrx2vlinest  48590  line2xlem  48602  itschlc0yqe  48609  itsclquadeu  48626