Theorem eqcoms 2773

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

Syntax hints:   → wi 4   = wceq 1563

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1803  df-cleq 2757

This theorem is referenced by:  gencbvex  3513  sbceq2a  3759  eqimss2  3998  uneqdifeq  4449  tppreq3  4721  ifpprsnss  4726  tpprceq3  4767  preqsnd  4820  prproe  4866  copsex2t  5466  snopeqop  5480  opthhausdorff0  5492  optocl  5746  relopabi  5800  cnvimassrndm  6141  cnveqb  6187  cnveq0  6188  unixpid  6275  reuop  6284  f0rn0  6753  fimadmfo  6791  f1ssf1  6843  tz6.12i  6897  fveqdmss  7063  fvcofneq  7078  funopsnOLD  7135  f1ocnvfv  7266  f1ocnvfvb  7267  cbvfo  7277  riotaeqimp  7383  ov6g  7564  tfindsg  7845  findsg  7882  mptcnfimad  7971  suppimacnv  8158  ectocld  8768  ecoptocl  8793  undifixp  8920  f1dmvrnfibi  9286  f1vrnfibi  9287  updjud  9908  card1  9942  prdom2  9978  sornom  10249  indpi  10880  ltlen  11299  eqlei  11308  squeeze0  12109  nn0ind-raph  12687  fzoopth  13782  injresinjlem  13810  fvf1tp  13813  modmuladd  13940  modmuladdnn0  13942  hashf1rn  14379  hashrabsn1  14401  hash1snb  14446  hashgt12el  14449  hashgt12el2  14450  hashfzp1  14458  hash2prde  14497  hash2pwpr  14503  fi1uzind  14534  brfi1indALT  14537  lswlgt0cl  14596  wrd2ind  14750  pfxccatin12lem2  14758  pfxccatin12lem3  14759  cshweqrep  14848  scshwfzeqfzo  14853  cshimadifsn  14856  cshimadifsn0  14857  2swrd2eqwrdeq  14980  wwlktovfo  14985  sgn3da  15128  rennim  15280  absmod0  15344  modfsummods  15835  mod2eq1n2dvds  16395  m1expe  16422  m1expo  16423  m1exp1  16424  nn0o1gt2  16429  flodddiv4  16463  cncongr1  16715  ge2nprmge4  16750  m1dvdsndvds  16848  cshwrepswhash1  17152  initoeu2lem1  18061  istos  18462  mgmsscl  18693  mndinvmod  18812  smndex1n0mnd  18964  symgfvne  19442  symgfix2  19477  symgextf1  19482  symgfixelsi  19496  psgnsn  19581  odbezout  19619  cntzcmnss  19902  frgpnabllem1  19934  ringinvnzdiv  20375  rngcinv  20713  psgndiflemB  21710  uvcendim  21957  selvvvval  22253  mamufacex  22514  smatvscl  22642  mavmulsolcl  22669  mdetunilem8  22737  pm2mpfo  22932  chpscmat  22960  chmaidscmat  22966  chfacfscmulgsum  22978  chfacfpmmulgsum  22982  txcn  23744  qtopeu  23834  reeff1o  26568  relogbcxpb  26910  logbgcd1irr  26917  fsumdvdsmul  27317  zabsle1  27418  2lgslem1c  27515  2lgsoddprmlem3  27536  2sq2  27555  2sqreultlem  27569  2sqreunnltlem  27572  2sqreulem3  27575  pntrlog2bndlem5  27703  ltlesnd  27897  upgrpredgv  29398  usgredg2vlem2  29485  ushgredgedg  29488  ushgredgedgloop  29490  uhgrspan1  29562  nb3grprlem1  29639  uvtxnbgrb  29660  cusgrsize2inds  29712  1egrvtxdg0  29770  uspgrloopvtxel  29775  finsumvtxdg2size  29809  rusgrpropnb  29842  ifpsnprss  29881  upgrwlkvtxedg  29903  uspgr2wlkeq  29904  wlkp1lem5  29934  wlkp1  29938  usgr2pth  30022  uspgrn2crct  30066  iswwlksnon  30111  wlkiswwlks1  30125  wlkiswwlks2lem3  30129  wwlksnextbi  30152  wwlksnredwwlkn0  30154  wwlksnextwrd  30155  wwlksnextsurj  30158  wwlksnextprop  30170  wspn0  30182  umgr2adedgwlkonALT  30205  umgr2adedgspth  30206  umgr2wlkon  30208  elwwlks2ons3  30213  elwwlks2on  30219  clwlkclwwlklem2a4  30257  clwlkclwwlklem2a  30258  clwlkclwwlkf1lem3  30266  clwwlkfo  30310  eleclclwwlknlem2  30321  erclwwlkntr  30331  hashecclwwlkn1  30337  umgrhashecclwwlk  30338  0wlkonlem1  30378  upgr1wlkdlem1  30405  1pthon2v  30413  upgr3v3e3cycl  30440  uhgr3cyclexlem  30441  upgr4cycl4dv4e  30445  eupth2lem3lem3  30490  eupth2lem3lem4  30491  1to2vfriswmgr  30539  frgrncvvdeqlem6  30564  frgrncvvdeqlem8  30566  frgrncvvdeqlem9  30567  frgrwopreglem2  30573  2clwwlk2clwwlk  30610  extwwlkfab  30612  numclwwlk1lem2f1  30617  numclwwlkovh  30633  numclwwlk2lem1  30636  numclwlk2lem2f  30637  cdj1i  32694  brabgaf  32863  br8d  32865  onvf1odlem1  35458  spthcycl  35492  goalrlem  35759  goalr  35760  fmlasucdisj  35762  satffunlem  35764  satffunlem1lem1  35765  satffunlem1lem2  35766  satffunlem2lem1  35767  satffunlem2lem2  35769  mthmb  35944  br8  36119  br4  36121  bj-snsetex  37460  bj-snglc  37466  copsex2d  37643  wl-dfcleq  38020  poimirlem20  38151  poimirlem26  38157  poimirlem27  38158  mblfinlem3  38170  mblfinlem4  38171  itg2addnclem  38182  indexdom  38245  ismgmOLD  38361  rngodm1dm2  38443  rngomndo  38446  rngoueqz  38451  zerdivemp1x  38458  opcon3b  39832  ps-1  40113  3atlem5  40123  4atex  40712  prjspvs  43204  iscard4  44121  pr2cv  44136  pm13.192  44984  iotavalsb  45007  relpfrlem  45527  fourierdlem32  46711  fourierdlem49  46727  fourierdlem64  46742  elprneb  47621  fveqvfvv  47632  funressnfv  47635  f1cof1b  47669  nvelim  47715  afvpcfv0  47738  afv0nbfvbi  47743  fnbrafvb  47746  tz6.12-afv  47765  afvco2  47768  ndmaovg  47776  afv2orxorb  47820  tz6.12-afv2  47832  tz6.12i-afv2  47835  f1oresf1o2  47883  nnmul2  47922  elsetpreimafvbi  47995  imasetpreimafvbijlemfo  48009  iccpartiltu  48026  fargshiftfv  48043  fargshiftf  48044  lswn0  48048  prsprel  48091  reupr  48126  2exopprim  48129  fmtnorec2lem  48149  2pwp1prm  48196  lighneallem2  48213  lighneallem3  48214  proththd  48221  ppivalnnprm  48232  ppivalnnnprmge6  48233  nn0o1gt2ALTV  48314  evenltle  48337  sbgoldbwt  48397  nnsum4primeseven  48420  nnsum4primesevenALTV  48421  clnbgrval  48442  dfvopnbgr2  48473  uhgrimedgi  48510  gricushgr  48537  clnbgrgrim  48554  grimedg  48555  cycl3grtri  48567  isubgr3stgrlem4  48589  uspgrlimlem1  48608  grlimgrtri  48623  gpgedg2ov  48686  gpgedg2iv  48687  pgnbgreunbgrlem1  48733  pgnbgreunbgrlem2lem3  48736  pgnbgreunbgrlem2  48737  pgnbgreunbgrlem4  48739  uspgropssxp  48764  lmod0rng  48849  lidldomn1  48851  zlidlring  48854  rngcinvALTV  48896  ztprmneprm  48978  lincext3  49087  zlmodzxznm  49128  suppdm  49141  elfzolborelfzop1  49150  nn0sumshdiglemB  49251  itcovalsucov  49299  lines  49362  rrx2vlinest  49372  line2xlem  49384  itschlc0yqe  49391  itsclquadeu  49408