Theorem eqcoms 2774

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2156  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2758

This theorem is used by:  gencbvex  3514  sbceq2a  3759  eqimss2  3999  uneqdifeq  4458  tppreq3  4730  ifpprsnss  4735  tpprceq3  4777  preqsnd  4829  prproe  4875  copsex2t  5480  snopeqop  5494  opthhausdorff0  5506  optocl  5760  relopabi  5814  cnvimassrndm  6154  cnveqb  6200  cnveq0  6201  unixpid  6292  reuop  6301  f0rn0  6770  fimadmfo  6808  f1ssf1  6860  tz6.12i  6914  fveqdmss  7080  fvcofneq  7095  funopsnOLD  7152  f1ocnvfv  7287  f1ocnvfvb  7288  cbvfo  7298  riotaeqimp  7406  ov6g  7587  tfindsg  7866  findsg  7903  mptcnfimad  7992  suppimacnv  8179  ectocld  8789  ecoptocl  8814  undifixp  8941  f1dmvrnfibi  9308  f1vrnfibi  9309  updjud  9939  card1  9973  prdom2  10009  sornom  10279  indpi  10910  ltlen  11329  eqlei  11338  squeeze0  12136  nn0ind-raph  12714  fzoopth  13810  injresinjlem  13838  fvf1tp  13842  modmuladd  13969  modmuladdnn0  13971  hashf1rn  14408  hashrabsn1  14430  hash1snb  14476  hashgt12el  14479  hashgt12el2  14480  hashfzp1  14488  hash2prde  14527  hash2pwpr  14533  fi1uzind  14564  brfi1indALT  14567  lswlgt0cl  14626  wrd2ind  14784  pfxccatin12lem2  14792  pfxccatin12lem3  14793  cshweqrep  14884  scshwfzeqfzo  14889  cshimadifsn  14892  cshimadifsn0  14893  2swrd2eqwrdeq  15016  wwlktovfo  15021  sgn3da  15164  rennim  15316  absmod0  15380  modfsummods  15871  mod2eq1n2dvds  16430  m1expe  16457  m1expo  16458  m1exp1  16459  nn0o1gt2  16464  flodddiv4  16498  cncongr1  16750  ge2nprmge4  16785  m1dvdsndvds  16883  cshwrepswhash1  17187  initoeu2lem1  18096  istos  18497  mgmsscl  18728  0gisid  18751  mndinvmod  18853  smndex1n0mnd  19005  symgfvne  19482  symgfix2  19517  symgextf1  19522  symgfixelsi  19536  psgnsn  19621  odbezout  19659  cntzcmnss  19942  frgpnabllem1  19974  ringinvnzdiv  20417  rngcinv  20773  psgndiflemB  21787  uvcendim  22034  selvvvval  22330  mamufacex  22590  smatvscl  22718  mavmulsolcl  22745  mdetunilem8  22813  pm2mpfo  23008  chpscmat  23036  chmaidscmat  23042  chfacfscmulgsum  23054  chfacfpmmulgsum  23058  txcn  23820  qtopeu  23910  reeff1o  26647  relogbcxpb  26989  logbgcd1irr  26996  fsumdvdsmul  27396  zabsle1  27497  2lgslem1c  27594  2lgsoddprmlem3  27615  2sq2  27634  2sqreultlem  27648  2sqreunnltlem  27651  2sqreulem3  27654  pntrlog2bndlem5  27782  ltlesnd  27976  upgrpredgv  29526  usgredg2vlem2  29613  ushgredgedg  29616  ushgredgedgloop  29618  uhgrspan1  29690  nb3grprlem1  29767  uvtxnbgrb  29788  cusgrsize2inds  29840  1egrvtxdg0  29898  uspgrloopvtxel  29903  finsumvtxdg2size  29937  rusgrpropnb  29970  ifpsnprss  30009  upgrwlkvtxedg  30031  uspgr2wlkeq  30032  wlkp1lem5  30062  wlkp1  30066  usgr2pth  30150  uspgrn2crct  30194  iswwlksnon  30239  wlkiswwlks1  30253  wlkiswwlks2lem3  30257  wwlksnextbi  30280  wwlksnredwwlkn0  30282  wwlksnextwrd  30283  wwlksnextsurj  30286  wwlksnextprop  30298  wspn0  30310  umgr2adedgwlkonALT  30333  umgr2adedgspth  30334  umgr2wlkon  30336  elwwlks2ons3  30341  elwwlks2on  30347  clwlkclwwlklem2a4  30385  clwlkclwwlklem2a  30386  clwlkclwwlkf1lem3  30394  clwwlkfo  30438  eleclclwwlknlem2  30449  erclwwlkntr  30459  hashecclwwlkn1  30465  umgrhashecclwwlk  30466  0wlkonlem1  30506  upgr1wlkdlem1  30533  1pthon2v  30541  upgr3v3e3cycl  30568  uhgr3cyclexlem  30569  upgr4cycl4dv4e  30573  eupth2lem3lem3  30618  eupth2lem3lem4  30619  1to2vfriswmgr  30667  frgrncvvdeqlem6  30692  frgrncvvdeqlem8  30694  frgrncvvdeqlem9  30695  frgrwopreglem2  30701  2clwwlk2clwwlk  30738  extwwlkfab  30740  numclwwlk1lem2f1  30745  numclwwlkovh  30761  numclwwlk2lem1  30764  numclwlk2lem2f  30765  cdj1i  32822  brabgaf  32988  br8d  32990  kardcard2b  35601  onvf1odlem1  35610  spthcycl  35641  goalrlem  35908  goalr  35909  fmlasucdisj  35911  satffunlem  35913  satffunlem1lem1  35914  satffunlem1lem2  35915  satffunlem2lem1  35916  satffunlem2lem2  35918  mthmb  36093  br8  36268  br4  36270  bj-snsetex  37639  bj-snglc  37645  copsex2d  37823  wl-dfcleq  38200  poimirlem20  38331  poimirlem26  38337  poimirlem27  38338  mblfinlem3  38350  mblfinlem4  38351  itg2addnclem  38362  indexdom  38425  ismgmOLD  38541  rngodm1dm2  38623  rngomndo  38626  rngoueqz  38631  zerdivemp1x  38638  opcon3b  40010  ps-1  40291  3atlem5  40301  4atex  40890  prjspvs  43382  iscard4  44299  pr2cv  44314  pm13.192  45160  iotavalsb  45183  relpfrlem  45702  fourierdlem32  46893  fourierdlem49  46909  fourierdlem64  46924  elprneb  47806  fveqvfvv  47817  funressnfv  47820  f1cof1b  47854  nvelim  47900  afvpcfv0  47923  afv0nbfvbi  47928  fnbrafvb  47931  tz6.12-afv  47950  afvco2  47953  ndmaovg  47961  afv2orxorb  48005  tz6.12-afv2  48017  tz6.12i-afv2  48020  f1oresf1o2  48068  nnmul2  48107  elsetpreimafvbi  48180  imasetpreimafvbijlemfo  48194  iccpartiltu  48211  fargshiftfv  48228  fargshiftf  48229  lswn0  48233  prsprel  48276  reupr  48311  2exopprim  48314  fmtnorec2lem  48334  2pwp1prm  48381  lighneallem2  48398  lighneallem3  48399  proththd  48406  ppivalnnprm  48417  ppivalnnnprmge6  48418  nn0o1gt2ALTV  48499  evenltle  48522  sbgoldbwt  48582  nnsum4primeseven  48605  nnsum4primesevenALTV  48606  clnbgrval  48627  dfvopnbgr2  48658  uhgrimedgi  48695  gricushgr  48722  clnbgrgrim  48739  grimedg  48740  cycl3grtri  48752  isubgr3stgrlem4  48774  uspgrlimlem1  48793  grlimgrtri  48808  gpgedg2ov  48871  gpgedg2iv  48872  pgnbgreunbgrlem1  48918  pgnbgreunbgrlem2lem3  48921  pgnbgreunbgrlem2  48922  pgnbgreunbgrlem4  48924  uspgropssxp  48949  lmod0rng  49034  lidldomn1  49036  zlidlring  49039  rngcinvALTV  49081  ztprmneprm  49167  lincext3  49276  zlmodzxznm  49317  suppdm  49330  elfzolborelfzop1  49339  nn0sumshdiglemB  49440  itcovalsucov  49488  lines  49551  rrx2vlinest  49561  line2xlem  49573  itschlc0yqe  49580  itsclquadeu  49597