Theorem eqcoms 2739

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

Syntax hints:   → wi 4   = wceq 1540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-9 2115  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1781  df-cleq 2723

This theorem is referenced by:  gencbvex  3535  sbceq2a  3789  eqimss2  4041  uneqdifeq  4492  tppreq3  4763  ifpprsnss  4768  tpprceq3  4807  preqsnd  4859  elpr2elpr  4869  prproe  4906  copsex2t  5492  copsex2gOLD  5494  snopeqop  5506  opthhausdorff0  5518  relopabi  5822  cnvimassrndm  6151  cnveqb  6195  cnveq0  6196  unixpid  6283  reuop  6292  f0rn0  6776  fimadmfo  6814  f1ssf1  6865  tz6.12i  6919  fveqdmss  7080  fvcofneq  7094  funopsn  7148  f1ocnvfv  7279  f1ocnvfvb  7280  cbvfo  7290  riotaeqimp  7395  ov6g  7575  tfindsg  7854  findsg  7894  suppimacnv  8164  suppssOLD  8185  ectocld  8784  ecoptocl  8807  undifixp  8934  phplem3OLD  9225  f1dmvrnfibi  9342  f1vrnfibi  9343  updjud  9935  card1  9969  pr2neOLD  10006  prdom2  10007  sornom  10278  indpi  10908  ltlen  11322  eqlei  11331  squeeze0  12124  nn0ind-raph  12669  injresinjlem  13759  modmuladd  13885  modmuladdnn0  13887  hashf1rn  14319  hashrabsn1  14341  hash1snb  14386  hashgt12el  14389  hashgt12el2  14390  hashfzp1  14398  hash2prde  14438  hash2pwpr  14444  fi1uzind  14465  brfi1indALT  14468  lswlgt0cl  14526  wrd2ind  14680  pfxccatin12lem2  14688  pfxccatin12lem3  14689  cshweqrep  14778  cshwsexaOLD  14782  scshwfzeqfzo  14784  cshimadifsn  14787  cshimadifsn0  14788  2swrd2eqwrdeq  14911  wwlktovfo  14916  rennim  15193  absmod0  15257  modfsummods  15746  mod2eq1n2dvds  16297  m1expe  16324  m1expo  16325  m1exp1  16326  nn0o1gt2  16331  flodddiv4  16363  cncongr1  16611  ge2nprmge4  16645  m1dvdsndvds  16738  cshwrepswhash1  17043  initoeu2lem1  17974  istos  18381  mgmsscl  18576  mndinvmod  18695  smndex1n0mnd  18835  symgfvne  19296  symgfix2  19332  symgextf1  19337  symgfixelsi  19351  psgnsn  19436  odbezout  19474  cntzcmnss  19757  frgpnabllem1  19789  ringinvnzdiv  20196  rngcinv  20529  psgndiflemB  21463  uvcendim  21712  mamufacex  22211  smatvscl  22346  mavmulsolcl  22373  mdetunilem8  22441  pm2mpfo  22636  chpscmat  22664  chmaidscmat  22670  chfacfscmulgsum  22682  chfacfpmmulgsum  22686  txcn  23450  qtopeu  23540  reeff1o  26299  relogbcxpb  26633  logbgcd1irr  26640  fsumdvdsmul  27041  zabsle1  27143  2lgslem1c  27240  2lgsoddprmlem3  27261  2sq2  27280  2sqreultlem  27294  2sqreunnltlem  27297  2sqreulem3  27300  pntrlog2bndlem5  27428  sltlend  27618  upgrpredgv  28833  usgredg2vlem2  28917  ushgredgedg  28920  ushgredgedgloop  28922  uhgrspan1  28994  nb3grprlem1  29071  uvtxnbgrb  29092  cusgrsize2inds  29144  1egrvtxdg0  29202  uspgrloopvtxel  29207  finsumvtxdg2size  29241  rusgrpropnb  29274  ifpsnprss  29314  upgrwlkvtxedg  29336  uspgr2wlkeq  29337  wlkp1lem5  29368  wlkp1  29372  usgr2pth  29455  uspgrn2crct  29496  iswwlksnon  29541  wlkiswwlks1  29555  wlkiswwlks2lem3  29559  wwlksnextbi  29582  wwlksnredwwlkn0  29584  wwlksnextwrd  29585  wwlksnextsurj  29588  wwlksnextprop  29600  wspn0  29612  umgr2adedgwlkonALT  29635  umgr2adedgspth  29636  umgr2wlkon  29638  elwwlks2ons3  29643  elwwlks2on  29647  clwlkclwwlklem2a4  29684  clwlkclwwlklem2a  29685  clwlkclwwlkf1lem3  29693  clwwlkfo  29737  eleclclwwlknlem2  29748  erclwwlkntr  29758  hashecclwwlkn1  29764  umgrhashecclwwlk  29765  0wlkonlem1  29805  upgr1wlkdlem1  29832  1pthon2v  29840  upgr3v3e3cycl  29867  uhgr3cyclexlem  29868  upgr4cycl4dv4e  29872  eupth2lem3lem3  29917  eupth2lem3lem4  29918  1to2vfriswmgr  29966  frgrncvvdeqlem6  29991  frgrncvvdeqlem8  29993  frgrncvvdeqlem9  29994  frgrwopreglem2  30000  2clwwlk2clwwlk  30037  extwwlkfab  30039  numclwwlk1lem2f1  30044  numclwwlkovh  30060  numclwwlk2lem1  30063  numclwlk2lem2f  30064  cdj1i  32120  brabgaf  32271  br8d  32273  sgn3da  34005  spthcycl  34585  goalrlem  34852  goalr  34853  fmlasucdisj  34855  satffunlem  34857  satffunlem1lem1  34858  satffunlem1lem2  34859  satffunlem2lem1  34860  satffunlem2lem2  34862  mthmb  35037  br8  35197  br4  35199  bj-snsetex  36310  bj-snglc  36316  copsex2d  36486  poimirlem20  36974  poimirlem26  36980  poimirlem27  36981  mblfinlem3  36993  mblfinlem4  36994  itg2addnclem  37005  indexdom  37068  ismgmOLD  37184  rngodm1dm2  37266  rngomndo  37269  rngoueqz  37274  zerdivemp1x  37281  opcon3b  38532  ps-1  38814  3atlem5  38824  4atex  39413  selvvvval  41622  prjspvs  41817  iscard4  42749  pr2cv  42764  pm13.192  43634  iotavalsb  43657  fourierdlem32  45316  fourierdlem49  45332  fourierdlem64  45347  elprneb  46200  fveqvfvv  46211  funressnfv  46214  f1cof1b  46246  nvelim  46292  afvpcfv0  46315  afv0nbfvbi  46320  fnbrafvb  46323  tz6.12-afv  46342  afvco2  46345  ndmaovg  46353  afv2orxorb  46397  tz6.12-afv2  46409  tz6.12i-afv2  46412  f1oresf1o2  46460  fzoopth  46496  elsetpreimafvbi  46520  imasetpreimafvbijlemfo  46534  iccpartiltu  46551  fargshiftfv  46568  fargshiftf  46569  lswn0  46573  prsprel  46616  reupr  46651  2exopprim  46654  fmtnorec2lem  46671  2pwp1prm  46718  lighneallem2  46735  lighneallem3  46736  proththd  46743  nn0o1gt2ALTV  46823  evenltle  46846  sbgoldbwt  46906  nnsum4primeseven  46929  nnsum4primesevenALTV  46930  isomushgr  46955  isomuspgrlem1  46956  uspgropssxp  46983  lmod0rng  47068  lidldomn1  47070  zlidlring  47073  rngcinvALTV  47115  ztprmneprm  47188  lincext3  47301  zlmodzxznm  47342  suppdm  47355  elfzolborelfzop1  47364  nn0sumshdiglemB  47470  itcovalsucov  47518  lines  47581  rrx2vlinest  47591  line2xlem  47603  itschlc0yqe  47610  itsclquadeu  47627