Theorem eqcoms 2769

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 2768	. 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 2155  ax-ext 2733

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

This theorem is used by:  gencbvex  3507  sbceq2a  3751  eqimss2  3990  uneqdifeq  4448  tppreq3  4720  ifpprsnss  4725  tpprceq3  4767  preqsnd  4819  prproe  4865  copsex2t  5464  snopeqop  5478  opthhausdorff0  5491  optocl  5745  relopabi  5800  cnvimassrndm  6141  cnveqb  6188  cnveq0  6189  unixpid  6280  reuop  6289  f0rn0  6759  fimadmfo  6797  f1ssf1  6849  tz6.12i  6903  fveqdmss  7070  fvcofneq  7085  funopsnOLD  7144  f1ocnvfv  7278  f1ocnvfvb  7279  cbvfo  7289  riotaeqimp  7395  ov6g  7576  tfindsg  7861  findsg  7898  mptcnfimad  7987  suppimacnv  8175  ectocld  8787  ecoptocl  8812  undifixp  8946  f1dmvrnfibi  9314  f1vrnfibi  9315  updjud  9996  card1  10030  prdom2  10066  sornom  10336  indpi  10973  ltlen  11392  eqlei  11401  squeeze0  12201  nn0ind-raph  12780  fzoopth  13877  injresinjlem  13905  fvf1tp  13909  modmuladd  14036  modmuladdnn0  14038  hashf1rn  14476  hashrabsn1  14498  hash1snb  14544  hashgt12el  14547  hashgt12el2  14548  hashfzp1  14556  hash2prde  14595  hash2pwpr  14601  fi1uzind  14632  brfi1indALT  14635  lswlgt0cl  14694  wrd2ind  14852  pfxccatin12lem2  14860  pfxccatin12lem3  14861  cshweqrep  14952  scshwfzeqfzo  14957  cshimadifsn  14960  cshimadifsn0  14961  2swrd2eqwrdeq  15086  wwlktovfo  15091  sgn3da  15234  rennim  15386  absmod0  15450  modfsummods  15940  mod2eq1n2dvds  16497  m1expe  16524  m1expo  16525  m1exp1  16526  nn0o1gt2  16531  flodddiv4  16565  cncongr1  16822  ge2nprmge4  16857  m1dvdsndvds  16956  cshwrepswhash1  17260  initoeu2lem1  18169  istos  18570  mgmsscl  18801  0gisid  18828  mndinvmod  18938  smndex1n0mnd  19091  symgfvne  19575  symgfix2  19610  symgextf1  19615  symgfixelsi  19629  psgnsn  19714  odbezout  19752  cntzcmnss  20035  frgpnabllem1  20067  ringinvnzdiv  20512  rngcinv  20869  psgndiflemB  21886  uvcendim  22133  selvvvval  22431  mamufacex  22691  smatvscl  22819  mavmulsolcl  22846  mdetunilem8  22914  pm2mpfo  23112  chpscmat  23140  chmaidscmat  23146  chfacfscmulgsum  23158  chfacfpmmulgsum  23162  txcn  23925  qtopeu  24015  reeff1o  26756  relogbcxpb  27097  logbgcd1irr  27104  fsumdvdsmul  27504  zabsle1  27605  2lgslem1c  27702  2lgsoddprmlem3  27723  2sq2  27742  2sqreultlem  27756  2sqreunnltlem  27759  2sqreulem3  27762  pntrlog2bndlem5  27890  ltlesnd  28114  upgrpredgv  29699  usgredg2vlem2  29789  ushgredgedg  29792  ushgredgedgloop  29794  uhgrspan1  29866  nb3grprlem1  29943  uvtxnbgrb  29964  cusgrsize2inds  30016  1egrvtxdg0  30074  uspgrloopvtxel  30079  finsumvtxdg2size  30113  rusgrpropnb  30146  ifpsnprss  30185  upgrwlkvtxedg  30207  uspgr2wlkeq  30208  wlkp1lem5  30238  wlkp1  30242  usgr2pth  30332  spthcycl  30374  uspgrn2crct  30379  iswwlksnon  30424  wlkiswwlks1  30438  wlkiswwlks2lem3  30442  wwlksnextbi  30465  wwlksnredwwlkn0  30467  wwlksnextwrd  30468  wwlksnextsurj  30471  wwlksnextprop  30483  wspn0  30495  umgr2adedgwlkonALT  30518  umgr2adedgspth  30519  umgr2wlkon  30521  elwwlks2ons3  30526  elwwlks2on  30532  clwlkclwwlklem2a4  30570  clwlkclwwlklem2a  30571  clwlkclwwlkf1lem3  30579  clwwlkfo  30623  eleclclwwlknlem2  30634  erclwwlkntr  30644  hashecclwwlkn1  30650  umgrhashecclwwlk  30651  0wlkonlem1  30691  upgr1wlkdlem1  30718  1pthon2v  30736  upgr3v3e3cycl  30763  uhgr3cyclexlem  30764  upgr4cycl4dv4e  30768  eupth2lem3lem3  30813  eupth2lem3lem4  30814  1to2vfriswmgr  30862  frgrncvvdeqlem6  30887  frgrncvvdeqlem8  30889  frgrncvvdeqlem9  30890  frgrwopreglem2  30896  2clwwlk2clwwlk  30933  extwwlkfab  30935  numclwwlk1lem2f1  30940  numclwwlkovh  30956  numclwwlk2lem1  30959  numclwlk2lem2f  30960  cdj1i  33017  brabgaf  33182  br8d  33184  kardcard2b  35806  onvf1odlem1  35855  goalrlem  36130  goalr  36131  fmlasucdisj  36133  satffunlem  36135  satffunlem1lem1  36136  satffunlem1lem2  36137  satffunlem2lem1  36138  satffunlem2lem2  36140  mthmb  36315  br8  36490  br4  36492  bj-snsetex  37846  bj-snglc  37852  copsex2d  38028  wl-dfcleq  38405  poimirlem20  38526  poimirlem26  38532  poimirlem27  38533  mblfinlem3  38545  mblfinlem4  38546  itg2addnclem  38557  indexdom  38636  ismgmOLD  38752  rngodm1dm2  38834  rngomndo  38837  rngoueqz  38842  zerdivemp1x  38849  opcon3b  40221  ps-1  40502  3atlem5  40512  4atex  41101  prjspvs  43600  iscard4  44492  pr2cv  44507  pm13.192  45353  iotavalsb  45376  relpfrlem  45895  fourierdlem32  47093  fourierdlem49  47109  fourierdlem64  47124  elprneb  48043  fveqvfvv  48054  funressnfv  48057  f1cof1b  48091  nvelim  48137  afvpcfv0  48160  afv0nbfvbi  48165  fnbrafvb  48168  tz6.12-afv  48187  afvco2  48190  ndmaovg  48198  afv2orxorb  48242  tz6.12-afv2  48254  tz6.12i-afv2  48257  f1oresf1o2  48305  nnmul2  48344  elsetpreimafvbi  48417  imasetpreimafvbijlemfo  48431  iccpartiltu  48448  fargshiftfv  48465  fargshiftf  48466  lswn0  48470  prsprel  48513  reupr  48548  2exopprim  48551  fmtnorec2lem  48571  2pwp1prm  48618  lighneallem2  48635  lighneallem3  48636  proththd  48643  ppivalnnprm  48654  ppivalnnnprmge6  48655  nn0o1gt2ALTV  48736  evenltle  48759  sbgoldbwt  48819  nnsum4primeseven  48842  nnsum4primesevenALTV  48843  clnbgrval  48864  dfvopnbgr2  48895  uhgrimedgi  48932  gricushgr  48959  clnbgrgrim  48976  grimedg  48977  cycl3grtri  48989  isubgr3stgrlem4  49011  uspgrlimlem1  49030  grlimgrtri  49045  gpgedg2ov  49108  gpgedg2iv  49109  pgnbgreunbgrlem1  49155  pgnbgreunbgrlem2lem3  49158  pgnbgreunbgrlem2  49159  pgnbgreunbgrlem4  49161  uspgropssxp  49186  lmod0rng  49270  lidldomn1  49272  zlidlring  49275  rngcinvALTV  49317  ztprmneprm  49403  lincext3  49512  zlmodzxznm  49553  suppdm  49566  elfzolborelfzop1  49575  nn0sumshdiglemB  49676  itcovalsucov  49724  lines  49787  rrx2vlinest  49797  line2xlem  49809  itschlc0yqe  49816  itsclquadeu  49833