Theorem anidms 566

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 412	. 2 ⊢ (𝜑 → (𝜑 → 𝜓))
3	2	pm2.43i 52	1 ⊢ (𝜑 → 𝜓)

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  sylancb  601  sylancbr  602  ru0  2133  eqeq12d  2753  rru  3739  dedth2v  4544  dedth3v  4545  dedth4v  4546  disjprsn  4673  opidg  4850  unisng  4883  intsng  4940  isso2i  5577  poinxp  5713  posn  5718  xpid11  5889  dfpo2  6262  predpoirr  6299  predfrirr  6300  f1oprswap  6827  f1o2sn  7097  residpr  7098  f1mpt  7217  f1eqcocnv  7257  isopolem  7301  3xpexg  7707  sqxpexg  7710  poxp  8080  poxp2  8095  poxp3  8102  oe0  8459  oecl  8474  nnmsucr  8563  ecopover  8770  enrefg  8933  php  9143  3xpfi  9233  dffi3  9346  infxpenlem  9935  isfin5  10221  isfin5-2  10313  pwfseqlem4a  10584  pwfseqlem4  10585  pwfseqlem5  10586  pwfseq  10587  nqereu  10852  halfnq  10899  ltsopr  10955  1idsr  11021  00sr  11022  sqgt0sr  11029  leid  11241  msqgt0  11669  msqge0  11670  recextlem1  11779  recextlem2  11780  recex  11781  div1  11843  cju  12153  2halves  12371  msqznn  12586  xrltnr  13045  xrleid  13077  iccid  13318  m1expeven  14044  sqneg  14050  sqcl  14053  nnsqcl  14063  qsqcl  14065  expubnd  14113  bernneq  14164  faclbnd  14225  faclbnd3  14227  hashfac  14393  leiso  14394  cjmulval  15080  fallrisefac  15960  sin2t  16114  cos2t  16115  divalglem0  16332  divalglem2  16334  gcd0id  16458  lcmid  16548  lcmgcdeq  16551  lcmfsn  16574  isprm5  16646  prslem  18232  pslem  18507  dirref  18536  efmndbasabf  18809  efmndhash  18813  efmndbasfi  18814  efmnd1bas  18830  submefmnd  18832  sgrp2nmndlem4  18865  grpsubid  18966  grp1inv  18990  cntzi  19270  symgbasfi  19320  symg1bas  19332  pgrpsubgsymg  19350  symgextfve  19360  pmtrfinv  19402  psgnsn  19461  ipeq0  21605  matsca2  22376  matbas2  22377  matplusgcell  22389  matsubgcell  22390  mamulid  22397  mamurid  22398  mattposcl  22409  mat1dimelbas  22427  mat1dimscm  22431  mat1dimmul  22432  m1detdiag  22553  mdetdiagid  22556  mdetunilem9  22576  pmatcoe1fsupp  22657  d1mat2pmat  22695  idcn  23213  hausdiag  23601  symgtgp  24062  ustref  24175  ustelimasn  24179  iducn  24238  ismet  24279  isxmet  24280  idnghm  24699  resubmet  24758  xrsxmet  24766  cphnm  25161  tcphnmval  25197  ipcau2  25202  tcphcphlem1  25203  tcphcphlem2  25204  tcphcph  25205  cmssmscld  25318  chordthmlem  26810  lesid  27747  lrrecpo  27949  subsid  28077  divs1  28212  zsoring  28417  ismot  28619  hmoval  30897  htth  31005  hvsubid  31113  hvnegid  31114  hv2times  31148  hiidrcl  31182  normval  31211  issh2  31296  chjidm  31607  normcan  31663  ho2times  31906  kbpj  32043  lnop0  32053  riesz3i  32149  leoprf  32215  leopsq  32216  cvnref  32378  gtiso  32790  fldextid  33836  prsss  34093  fineqvnttrclse  35299  deranglem  35379  elfix2  36115  linedegen  36356  filnetlem2  36592  matunitlindflem2  37865  matunitlindf  37866  ftc1anclem3  37943  prdsbnd2  38043  reheibor  38087  ismgmOLD  38098  opidon2OLD  38102  exidreslem  38125  rngo2  38155  opideq  38591  eldmcoss2  38797  mzpf  43090  acongrep  43334  ttac  43390  mendval  43533  iocinico  43566  iocmbl  43567  seff  44662  sblpnf  44663  sigarid  47213  cnambpcma  47651  2leaddle2  47655  grlicref  48369  clintopval  48561  2arymaptfv  49008  2arymaptfo  49011  itcoval2  49021  itcoval3  49022  resipos  49331  nelsubclem  49423  initoo2  49588  termoo2  49589  setc1onsubc  49958