Theorem eqcoms 2746

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

Syntax hints:   → wi 4   = wceq 1539

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-cleq 2730

This theorem is referenced by:  gencbvex  3478  sbceq2a  3723  eqimss2  3974  uneqdifeq  4420  tppreq3  4692  ifpprsnss  4697  tpprceq3  4734  preqsnd  4786  elpr2elpr  4796  prproe  4834  copsex2t  5400  copsex2gOLD  5402  snopeqop  5414  opthhausdorff0  5426  relopabi  5721  cnvimassrndm  6044  cnveqb  6088  cnveq0  6089  unixpid  6176  reuop  6185  f0rn0  6643  fimadmfo  6681  f1ssf1  6731  tz6.12i  6782  fveqdmss  6938  fvcofneq  6951  funopsn  7002  f1ocnvfv  7131  f1ocnvfvb  7132  cbvfo  7141  riotaeqimp  7239  ov6g  7414  tfindsg  7682  findsg  7720  suppimacnv  7961  suppssOLD  7982  ectocld  8531  ecoptocl  8554  undifixp  8680  phplem3  8894  f1dmvrnfibi  9033  f1vrnfibi  9034  updjud  9623  card1  9657  pr2ne  9692  prdom2  9693  sornom  9964  indpi  10594  ltlen  11006  eqlei  11015  squeeze0  11808  nn0ind-raph  12350  injresinjlem  13435  modmuladd  13561  modmuladdnn0  13563  hashf1rn  13995  hashrabsn1  14017  hash1snb  14062  hashgt12el  14065  hashgt12el2  14066  hashfzp1  14074  hash2prde  14112  hash2pwpr  14118  fi1uzind  14139  brfi1indALT  14142  lswlgt0cl  14200  wrd2ind  14364  pfxccatin12lem2  14372  pfxccatin12lem3  14373  cshweqrep  14462  cshwsexa  14465  scshwfzeqfzo  14467  cshimadifsn  14470  cshimadifsn0  14471  2swrd2eqwrdeq  14594  wwlktovfo  14601  rennim  14878  absmod0  14943  modfsummods  15433  mod2eq1n2dvds  15984  m1expe  16011  m1expo  16012  m1exp1  16013  nn0o1gt2  16018  flodddiv4  16050  cncongr1  16300  ge2nprmge4  16334  m1dvdsndvds  16427  cshwrepswhash1  16732  initoeu2lem1  17645  istos  18051  mgmsscl  18246  mndinvmod  18330  smndex1n0mnd  18466  symgfvne  18903  symgfix2  18939  symgextf1  18944  symgfixelsi  18958  psgnsn  19043  odbezout  19080  cntzcmnss  19357  frgpnabllem1  19389  ringinvnzdiv  19747  psgndiflemB  20717  uvcendim  20964  mamufacex  21448  smatvscl  21581  mavmulsolcl  21608  mdetunilem8  21676  pm2mpfo  21871  chpscmat  21899  chmaidscmat  21905  chfacfscmulgsum  21917  chfacfpmmulgsum  21921  txcn  22685  qtopeu  22775  reeff1o  25511  relogbcxpb  25842  logbgcd1irr  25849  zabsle1  26349  2lgslem1c  26446  2lgsoddprmlem3  26467  2sq2  26486  2sqreultlem  26500  2sqreunnltlem  26503  2sqreulem3  26506  pntrlog2bndlem5  26634  upgrpredgv  27412  usgredg2vlem2  27496  ushgredgedg  27499  ushgredgedgloop  27501  uhgrspan1  27573  nb3grprlem1  27650  uvtxnbgrb  27671  cusgrsize2inds  27723  1egrvtxdg0  27781  uspgrloopvtxel  27786  finsumvtxdg2size  27820  rusgrpropnb  27853  ifpsnprss  27892  upgrwlkvtxedg  27914  uspgr2wlkeq  27915  wlkp1lem5  27947  wlkp1  27951  usgr2pth  28033  uspgrn2crct  28074  iswwlksnon  28119  wlkiswwlks1  28133  wlkiswwlks2lem3  28137  wwlksnextbi  28160  wwlksnredwwlkn0  28162  wwlksnextwrd  28163  wwlksnextsurj  28166  wwlksnextprop  28178  wspn0  28190  umgr2adedgwlkonALT  28213  umgr2adedgspth  28214  umgr2wlkon  28216  elwwlks2ons3  28221  elwwlks2on  28225  clwlkclwwlklem2a4  28262  clwlkclwwlklem2a  28263  clwlkclwwlkf1lem3  28271  clwwlkfo  28315  eleclclwwlknlem2  28326  erclwwlkntr  28336  hashecclwwlkn1  28342  umgrhashecclwwlk  28343  0wlkonlem1  28383  upgr1wlkdlem1  28410  1pthon2v  28418  upgr3v3e3cycl  28445  uhgr3cyclexlem  28446  upgr4cycl4dv4e  28450  eupth2lem3lem3  28495  eupth2lem3lem4  28496  1to2vfriswmgr  28544  frgrncvvdeqlem6  28569  frgrncvvdeqlem8  28571  frgrncvvdeqlem9  28572  frgrwopreglem2  28578  2clwwlk2clwwlk  28615  extwwlkfab  28617  numclwwlk1lem2f1  28622  numclwwlkovh  28638  numclwwlk2lem1  28641  numclwlk2lem2f  28642  cdj1i  30696  brabgaf  30849  br8d  30851  sgn3da  32408  spthcycl  32991  goalrlem  33258  goalr  33259  fmlasucdisj  33261  satffunlem  33263  satffunlem1lem1  33264  satffunlem1lem2  33265  satffunlem2lem1  33266  satffunlem2lem2  33268  mthmb  33443  br8  33629  br4  33631  bj-snsetex  35080  bj-snglc  35086  copsex2d  35237  poimirlem20  35724  poimirlem26  35730  poimirlem27  35731  mblfinlem3  35743  mblfinlem4  35744  itg2addnclem  35755  indexdom  35819  ismgmOLD  35935  rngodm1dm2  36017  rngomndo  36020  rngoueqz  36025  zerdivemp1x  36032  opcon3b  37137  ps-1  37418  3atlem5  37428  4atex  38017  prjspvs  40370  iscard4  41038  pr2cv  41044  pm13.192  41917  iotavalsb  41940  fourierdlem32  43570  fourierdlem49  43586  fourierdlem64  43601  elprneb  44410  fveqvfvv  44421  funressnfv  44424  f1cof1b  44456  nvelim  44502  afvpcfv0  44525  afv0nbfvbi  44530  fnbrafvb  44533  tz6.12-afv  44552  afvco2  44555  ndmaovg  44563  afv2orxorb  44607  tz6.12-afv2  44619  tz6.12i-afv2  44622  f1oresf1o2  44670  fzoopth  44707  elsetpreimafvbi  44731  imasetpreimafvbijlemfo  44745  iccpartiltu  44762  fargshiftfv  44779  fargshiftf  44780  lswn0  44784  prsprel  44827  reupr  44862  2exopprim  44865  fmtnorec2lem  44882  2pwp1prm  44929  lighneallem2  44946  lighneallem3  44947  proththd  44954  nn0o1gt2ALTV  45034  evenltle  45057  sbgoldbwt  45117  nnsum4primeseven  45140  nnsum4primesevenALTV  45141  isomushgr  45166  isomuspgrlem1  45167  uspgropssxp  45194  lmod0rng  45314  lidldomn1  45367  zlidlring  45374  rngcinv  45427  rngcinvALTV  45439  ringcinv  45478  ringcinvALTV  45502  ztprmneprm  45571  lincext3  45685  zlmodzxznm  45726  suppdm  45739  elfzolborelfzop1  45748  nn0sumshdiglemB  45854  itcovalsucov  45902  lines  45965  rrx2vlinest  45975  line2xlem  45987  itschlc0yqe  45994  itsclquadeu  46011