Theorem eqcoms 2737

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

Syntax hints:   → wi 4   = wceq 1540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721

This theorem is referenced by:  gencbvex  3498  sbceq2a  3756  eqimss2  3997  uneqdifeq  4446  tppreq3  4713  ifpprsnss  4718  tpprceq3  4758  preqsnd  4813  prproe  4859  copsex2t  5439  snopeqop  5453  opthhausdorff0  5465  optocl  5717  relopabi  5769  cnvimassrndm  6105  cnveqb  6149  cnveq0  6150  unixpid  6236  reuop  6245  f0rn0  6713  fimadmfo  6749  f1ssf1  6800  tz6.12i  6852  fveqdmss  7016  fvcofneq  7031  funopsn  7086  f1ocnvfv  7219  f1ocnvfvb  7220  cbvfo  7230  riotaeqimp  7336  ov6g  7517  tfindsg  7801  findsg  7837  mptcnfimad  7928  suppimacnv  8114  ectocld  8716  ecoptocl  8741  undifixp  8868  f1dmvrnfibi  9250  f1vrnfibi  9251  updjud  9849  card1  9883  prdom2  9919  sornom  10190  indpi  10820  ltlen  11235  eqlei  11244  squeeze0  12046  nn0ind-raph  12594  fzoopth  13683  injresinjlem  13708  fvf1tp  13711  modmuladd  13838  modmuladdnn0  13840  hashf1rn  14277  hashrabsn1  14299  hash1snb  14344  hashgt12el  14347  hashgt12el2  14348  hashfzp1  14356  hash2prde  14395  hash2pwpr  14401  fi1uzind  14432  brfi1indALT  14435  lswlgt0cl  14494  wrd2ind  14647  pfxccatin12lem2  14655  pfxccatin12lem3  14656  cshweqrep  14745  cshwsexaOLD  14749  scshwfzeqfzo  14751  cshimadifsn  14754  cshimadifsn0  14755  2swrd2eqwrdeq  14878  wwlktovfo  14883  rennim  15164  absmod0  15228  modfsummods  15718  mod2eq1n2dvds  16276  m1expe  16303  m1expo  16304  m1exp1  16305  nn0o1gt2  16310  flodddiv4  16344  cncongr1  16596  ge2nprmge4  16630  m1dvdsndvds  16728  cshwrepswhash1  17032  initoeu2lem1  17939  istos  18340  mgmsscl  18537  mndinvmod  18656  smndex1n0mnd  18804  symgfvne  19278  symgfix2  19313  symgextf1  19318  symgfixelsi  19332  psgnsn  19417  odbezout  19455  cntzcmnss  19738  frgpnabllem1  19770  ringinvnzdiv  20204  rngcinv  20540  psgndiflemB  21525  uvcendim  21772  mamufacex  22299  smatvscl  22427  mavmulsolcl  22454  mdetunilem8  22522  pm2mpfo  22717  chpscmat  22745  chmaidscmat  22751  chfacfscmulgsum  22763  chfacfpmmulgsum  22767  txcn  23529  qtopeu  23619  reeff1o  26373  relogbcxpb  26713  logbgcd1irr  26720  fsumdvdsmul  27121  zabsle1  27223  2lgslem1c  27320  2lgsoddprmlem3  27341  2sq2  27360  2sqreultlem  27374  2sqreunnltlem  27377  2sqreulem3  27380  pntrlog2bndlem5  27508  sltlend  27699  upgrpredgv  29102  usgredg2vlem2  29189  ushgredgedg  29192  ushgredgedgloop  29194  uhgrspan1  29266  nb3grprlem1  29343  uvtxnbgrb  29364  cusgrsize2inds  29417  1egrvtxdg0  29475  uspgrloopvtxel  29480  finsumvtxdg2size  29514  rusgrpropnb  29547  ifpsnprss  29586  upgrwlkvtxedg  29608  uspgr2wlkeq  29609  wlkp1lem5  29639  wlkp1  29643  usgr2pth  29727  uspgrn2crct  29771  iswwlksnon  29816  wlkiswwlks1  29830  wlkiswwlks2lem3  29834  wwlksnextbi  29857  wwlksnredwwlkn0  29859  wwlksnextwrd  29860  wwlksnextsurj  29863  wwlksnextprop  29875  wspn0  29887  umgr2adedgwlkonALT  29910  umgr2adedgspth  29911  umgr2wlkon  29913  elwwlks2ons3  29918  elwwlks2on  29922  clwlkclwwlklem2a4  29959  clwlkclwwlklem2a  29960  clwlkclwwlkf1lem3  29968  clwwlkfo  30012  eleclclwwlknlem2  30023  erclwwlkntr  30033  hashecclwwlkn1  30039  umgrhashecclwwlk  30040  0wlkonlem1  30080  upgr1wlkdlem1  30107  1pthon2v  30115  upgr3v3e3cycl  30142  uhgr3cyclexlem  30143  upgr4cycl4dv4e  30147  eupth2lem3lem3  30192  eupth2lem3lem4  30193  1to2vfriswmgr  30241  frgrncvvdeqlem6  30266  frgrncvvdeqlem8  30268  frgrncvvdeqlem9  30269  frgrwopreglem2  30275  2clwwlk2clwwlk  30312  extwwlkfab  30314  numclwwlk1lem2f1  30319  numclwwlkovh  30335  numclwwlk2lem1  30338  numclwlk2lem2f  30339  cdj1i  32395  brabgaf  32569  br8d  32571  sgn3da  32792  onvf1odlem1  35075  spthcycl  35101  goalrlem  35368  goalr  35369  fmlasucdisj  35371  satffunlem  35373  satffunlem1lem1  35374  satffunlem1lem2  35375  satffunlem2lem1  35376  satffunlem2lem2  35378  mthmb  35553  br8  35728  br4  35730  bj-snsetex  36936  bj-snglc  36942  copsex2d  37112  poimirlem20  37619  poimirlem26  37625  poimirlem27  37626  mblfinlem3  37638  mblfinlem4  37639  itg2addnclem  37650  indexdom  37713  ismgmOLD  37829  rngodm1dm2  37911  rngomndo  37914  rngoueqz  37919  zerdivemp1x  37926  opcon3b  39174  ps-1  39456  3atlem5  39466  4atex  40055  selvvvval  42558  prjspvs  42583  iscard4  43506  pr2cv  43521  pm13.192  44383  iotavalsb  44406  relpfrlem  44927  fourierdlem32  46121  fourierdlem49  46137  fourierdlem64  46152  elprneb  47014  fveqvfvv  47025  funressnfv  47028  f1cof1b  47062  nvelim  47108  afvpcfv0  47131  afv0nbfvbi  47136  fnbrafvb  47139  tz6.12-afv  47158  afvco2  47161  ndmaovg  47169  afv2orxorb  47213  tz6.12-afv2  47225  tz6.12i-afv2  47228  f1oresf1o2  47276  elsetpreimafvbi  47376  imasetpreimafvbijlemfo  47390  iccpartiltu  47407  fargshiftfv  47424  fargshiftf  47425  lswn0  47429  prsprel  47472  reupr  47507  2exopprim  47510  fmtnorec2lem  47527  2pwp1prm  47574  lighneallem2  47591  lighneallem3  47592  proththd  47599  nn0o1gt2ALTV  47679  evenltle  47702  sbgoldbwt  47762  nnsum4primeseven  47785  nnsum4primesevenALTV  47786  clnbgrval  47807  dfvopnbgr2  47838  uhgrimedgi  47875  gricushgr  47902  clnbgrgrim  47919  grimedg  47920  cycl3grtri  47932  isubgr3stgrlem4  47954  uspgrlimlem1  47973  grlimgrtri  47988  gpgedg2ov  48051  gpgedg2iv  48052  pgnbgreunbgrlem1  48098  pgnbgreunbgrlem2lem3  48101  pgnbgreunbgrlem2  48102  pgnbgreunbgrlem4  48104  uspgropssxp  48129  lmod0rng  48214  lidldomn1  48216  zlidlring  48219  rngcinvALTV  48261  ztprmneprm  48332  lincext3  48442  zlmodzxznm  48483  suppdm  48496  elfzolborelfzop1  48505  nn0sumshdiglemB  48606  itcovalsucov  48654  lines  48717  rrx2vlinest  48727  line2xlem  48739  itschlc0yqe  48746  itsclquadeu  48763