Theorem eqcoms 2771

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 2770	. 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 1945  ax-6 2002  ax-7 2043  ax-9 2157  ax-ext 2735

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

This theorem is used by:  gencbvex  3510  sbceq2a  3754  eqimss2  3972  uneqdifeq  4451  tppreq3  4720  ifpprsnss  4725  tpprceq3  4767  preqsnd  4817  prproe  4836  nvelim  5277  copsex2t  5468  snopeqop  5482  opthhausdorff0  5495  optocl  5750  relopabiOLD  5806  cnvimassrndmOLD  6212  unixpid  6305  reuop  6314  f0rn0  6789  fimadmfo  6827  f1ssf1  6880  tz6.12i  6934  fveqdmss  7102  fvcofneq  7117  funopsnOLD  7176  f1ocnvfv  7309  f1ocnvfvb  7310  cbvfo  7320  riotaeqimp  7426  ov6g  7608  tfindsg  7896  findsg  7933  mptcnfimad  8022  suppimacnv  8219  ectocld  8831  ecoptocl  8856  undifixp  8990  f1dmvrnfibi  9358  f1vrnfibi  9359  updjud  10042  card1  10076  prdom2  10112  sornom  10382  indpi  11019  ltlen  11438  eqlei  11447  squeeze0  12247  nn0ind-raph  12826  fzoopth  13924  injresinjlem  13952  fvf1tp  13956  modmuladd  14083  modmuladdnn0  14085  hashf1rn  14523  hashrabsn1  14545  hash1snb  14591  hashgt12el  14594  hashgt12el2  14595  hashfzp1  14603  hash2prde  14642  hash2pwpr  14648  fi1uzind  14679  brfi1indALT  14682  lswlgt0cl  14741  wrd2ind  14900  pfxccatin12lem2  14908  pfxccatin12lem3  14909  cshweqrep  15000  scshwfzeqfzo  15005  cshimadifsn  15008  cshimadifsn0  15009  2swrd2eqwrdeq  15135  wwlktovfo  15140  sgn3da  15283  rennim  15435  absmod0  15499  modfsummods  15989  mod2eq1n2dvds  16546  m1expe  16573  m1expo  16574  m1exp1  16575  nn0o1gt2  16580  flodddiv4  16614  cncongr1  16871  ge2nprmge4  16906  m1dvdsndvds  17005  cshwrepswhash1  17309  initoeu2lem1  18218  istos  18619  mgmsscl  18850  0gisid  18877  mndinvmod  18987  smndex1n0mnd  19140  symgfvne  19625  symgfix2  19660  symgextf1  19665  symgfixelsi  19679  psgnsn  19764  odbezout  19802  cntzcmnss  20085  frgpnabllem1  20117  ringinvnzdiv  20562  rngcinv  20919  psgndiflemB  21936  uvcendim  22183  selvvvval  22481  mamufacex  22741  smatvscl  22869  mavmulsolcl  22896  mdetunilem8  22964  pm2mpfo  23162  chpscmat  23190  chmaidscmat  23196  chfacfscmulgsum  23208  chfacfpmmulgsum  23212  txcn  23975  qtopeu  24065  reeff1o  26804  relogbcxpb  27145  logbgcd1irr  27152  fsumdvdsmul  27552  zabsle1  27653  2lgslem1c  27750  2lgsoddprmlem3  27771  2sq2  27790  2sqreultlem  27804  2sqreunnltlem  27807  2sqreulem3  27810  pntrlog2bndlem5  27938  ltlesnd  28162  upgrpredgv  29747  usgredg2vlem2  29837  ushgredgedg  29840  ushgredgedgloop  29842  uhgrspan1  29914  nb3grprlem1  29991  uvtxnbgrb  30012  cusgrsize2inds  30064  1egrvtxdg0  30122  uspgrloopvtxel  30127  finsumvtxdg2size  30161  rusgrpropnb  30194  ifpsnprss  30233  upgrwlkvtxedg  30255  uspgr2wlkeq  30256  wlkp1lem5  30286  wlkp1  30290  usgr2pth  30380  spthcycl  30422  uspgrn2crct  30427  iswwlksnon  30472  wlkiswwlks1  30486  wlkiswwlks2lem3  30490  wwlksnextbi  30513  wwlksnredwwlkn0  30515  wwlksnextwrd  30516  wwlksnextsurj  30519  wwlksnextprop  30531  wspn0  30543  umgr2adedgwlkonALT  30566  umgr2adedgspth  30567  umgr2wlkon  30569  elwwlks2ons3  30574  elwwlks2on  30580  clwlkclwwlklem2a4  30618  clwlkclwwlklem2a  30619  clwlkclwwlkf1lem3  30627  clwwlkfo  30671  eleclclwwlknlem2  30682  erclwwlkntr  30692  hashecclwwlkn1  30698  umgrhashecclwwlk  30699  0wlkonlem1  30739  upgr1wlkdlem1  30766  1pthon2v  30784  upgr3v3e3cycl  30811  uhgr3cyclexlem  30812  upgr4cycl4dv4e  30816  eupth2lem3lem3  30861  eupth2lem3lem4  30862  1to2vfriswmgr  30910  frgrncvvdeqlem6  30935  frgrncvvdeqlem8  30937  frgrncvvdeqlem9  30938  frgrwopreglem2  30944  2clwwlk2clwwlk  30981  extwwlkfab  30983  numclwwlk1lem2f1  30988  numclwwlkovh  31004  numclwwlk2lem1  31007  numclwlk2lem2f  31008  cdj1i  33065  brabgaf  33272  br8d  33274  kardcard2b  35933  onvf1odlem1  36031  onprcf1acwevdlem2  36046  goalrlem  36328  goalr  36329  fmlasucdisj  36331  satffunlem  36333  satffunlem1lem1  36334  satffunlem1lem2  36335  satffunlem2lem1  36336  satffunlem2lem2  36338  mthmb  36513  br8  36699  br4  36701  bj-snsetex  38054  bj-snglc  38060  copsex2d  38252  wl-dfcleq  38629  poimirlem20  38750  poimirlem26  38756  poimirlem27  38757  mblfinlem3  38769  mblfinlem4  38770  itg2addnclem  38781  indexdom  38860  ismgmOLD  38976  rngodm1dm2  39058  rngomndo  39061  rngoueqz  39066  zerdivemp1x  39073  opcon3b  40445  ps-1  40726  3atlem5  40736  4atex  41325  prjspvs  43831  iscard4  44726  pr2cv  44741  pm13.192  45586  iotavalsb  45608  relpfrlem  46138  fourierdlem32  47354  fourierdlem49  47370  fourierdlem64  47385  elprneb  48304  fveqvfvv  48315  funressnfv  48318  f1cof1b  48352  afvpcfv0  48421  afv0nbfvbi  48426  fnbrafvb  48429  tz6.12-afv  48448  afvco2  48451  ndmaovg  48459  afv2orxorb  48503  tz6.12-afv2  48515  tz6.12i-afv2  48518  f1oresf1o2  48566  nnmul2  48605  elsetpreimafvbi  48678  imasetpreimafvbijlemfo  48692  iccpartiltu  48709  fargshiftfv  48726  fargshiftf  48727  lswn0  48731  prsprel  48774  reupr  48809  2exopprim  48812  fmtnorec2lem  48832  2pwp1prm  48879  lighneallem2  48896  lighneallem3  48897  proththd  48904  ppivalnnprm  48915  ppivalnnnprmge6  48916  nn0o1gt2ALTV  48997  evenltle  49020  sbgoldbwt  49080  nnsum4primeseven  49103  nnsum4primesevenALTV  49104  clnbgrval  49125  dfvopnbgr2  49156  uhgrimedgi  49193  gricushgr  49220  clnbgrgrim  49237  grimedg  49238  cycl3grtri  49250  isubgr3stgrlem4  49272  uspgrlimlem1  49291  grlimgrtri  49306  gpgedg2ov  49369  gpgedg2iv  49370  pgnbgreunbgrlem1  49416  pgnbgreunbgrlem2lem3  49419  pgnbgreunbgrlem2  49420  pgnbgreunbgrlem4  49422  uspgropssxp  49447  lmod0rng  49531  lidldomn1  49533  zlidlring  49536  rngcinvALTV  49578  ztprmneprm  49664  lincext3  49773  zlmodzxznm  49814  suppdm  49827  elfzolborelfzop1  49836  nn0sumshdiglemB  49937  itcovalsucov  49985  lines  50049  rrx2vlinest  50058  line2xlem  50070  itschlc0yqe  50077  itsclquadeu  50094