Theorem anidms 576

Description: Inference from idempotent law for conjunction. (Contributed by NM, 15-Jun-1994.)

Hypothesis

Ref	Expression
anidms.1	⊢ ((𝜑 ∧ 𝜑) → 𝜓)

Assertion

Ref	Expression
anidms	⊢ (𝜑 → 𝜓)

Proof of Theorem anidms

Step	Hyp	Ref	Expression
1		anidms.1	. . 3 ⊢ ((𝜑 ∧ 𝜑) → 𝜓)
2	1	ex 417	. 2 ⊢ (𝜑 → (𝜑 → 𝜓))
3	2	pm2.43i 53	1 ⊢ (𝜑 → 𝜓)

Syntax hints:   → wi 4   ∧ wa 400

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 210  df-an 401

This theorem is referenced by:  sylancb  611  sylancbr  612  ru0  2162  eqeq12d  2779  rru  3743  dedth2v  4551  dedth3v  4552  dedth4v  4553  disjprsn  4681  opidg  4858  unisng  4891  intsng  4949  isso2i  5608  poinxp  5744  posn  5749  xpid11  5924  dfpo2  6299  predpoirr  6336  predfrirr  6337  f1oprswap  6868  f1o2sn  7140  residpr  7141  f1mpt  7261  f1eqcocnv  7301  isopolem  7345  3xpexg  7752  sqxpexg  7755  poxp  8125  poxp2  8140  poxp3  8147  oe0  8508  oecl  8523  nnmsucr  8612  ecopover  8820  enrefg  8982  php  9192  3xpfi  9281  dffi3  9392  elirrv  9560  infxpenlem  9998  isfin5  10284  isfin5-2  10376  pwfseqlem4a  10647  pwfseqlem4  10648  pwfseqlem5  10649  pwfseq  10650  nqereu  10915  halfnq  10962  ltsopr  11018  1idsr  11084  00sr  11085  sqgt0sr  11092  leid  11307  msqgt0  11735  msqge0  11736  recextlem1  11845  recextlem2  11846  recex  11847  div1  11905  cju  12215  2halves  12463  msqznn  12679  xrltnr  13145  xrleid  13177  iccid  13418  m1expeven  14147  sqneg  14153  sqcl  14156  nnsqcl  14166  qsqcl  14168  expubnd  14216  bernneq  14267  faclbnd  14328  faclbnd3  14330  hashfac  14497  leiso  14498  cjmulval  15198  fallrisefac  16081  sin2t  16234  cos2t  16235  divalglem0  16452  divalglem2  16454  gcd0id  16578  lcmid  16668  lcmgcdeq  16671  lcmfsn  16694  isprm5  16767  prslem  18354  pslem  18629  dirref  18658  efmndbasabf  18932  efmndhash  18936  efmndbasfi  18937  efmnd1bas  18953  submefmnd  18955  sgrp2nmndlem4  18991  grpsubid  19091  grp1inv  19115  cntzi  19400  symgbasfi  19450  symg1bas  19462  pgrpsubgsymg  19480  symgextfve  19490  pmtrfinv  19532  psgnsn  19591  ipeq0  21769  matsca2  22558  matbas2  22559  matplusgcell  22571  matsubgcell  22572  mamulid  22579  mamurid  22580  mattposcl  22591  mat1dimelbas  22609  mat1dimscm  22613  mat1dimmul  22614  m1detdiag  22735  mdetdiagid  22738  mdetunilem9  22758  pmatcoe1fsupp  22839  d1mat2pmat  22877  idcn  23395  hausdiag  23783  symgtgp  24244  ustref  24357  ustelimasn  24361  iducn  24420  ismet  24461  isxmet  24462  idnghm  24881  resubmet  24940  xrsxmet  24948  cphnm  25333  tcphnmval  25369  ipcau2  25374  tcphcphlem1  25375  tcphcphlem2  25376  tcphcph  25377  cmssmscld  25490  chordthmlem  26978  lesid  27912  lrrecpo  28115  subsid  28243  divs1  28378  zsoring  28583  ismot  28785  hmoval  31143  htth  31251  hvsubid  31359  hvnegid  31360  hv2times  31394  hiidrcl  31428  normval  31457  issh2  31542  chjidm  31853  normcan  31909  ho2times  32152  kbpj  32289  lnop0  32299  riesz3i  32395  leoprf  32461  leopsq  32462  cvnref  32624  gtiso  33027  fldextid  34030  prsss  34287  fineqvnttrclse  35518  deranglem  35639  elfix2  36375  linedegen  36616  filnetlem2  36871  matunitlindflem2  38249  matunitlindf  38250  ftc1anclem3  38327  prdsbnd2  38427  reheibor  38471  ismgmOLD  38482  opidon2OLD  38486  exidreslem  38509  rngo2  38539  opideq  38973  eldmcoss2  39179  mzpf  43450  acongrep  43690  ttac  43746  mendval  43889  iocinico  43922  iocmbl  43923  seff  45002  sblpnf  45003  sigarid  47555  cnambpcma  48014  2leaddle2  48018  grlicref  48760  clintopval  48952  2arymaptfv  49414  2arymaptfo  49417  itcoval2  49427  itcoval3  49428  resipos  49736  nelsubclem  49828  initoo2  49993  termoo2  49994  setc1onsubc  50363