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  600  sylancbr  601  ru0  2127  eqeq12d  2751  rru  3762  dedth2v  4563  dedth3v  4564  dedth4v  4565  disjprsn  4690  opidg  4868  unisng  4901  intsng  4959  isso2i  5598  poinxp  5735  posn  5740  xpid11  5912  dfpo2  6285  predpoirr  6322  predfrirr  6323  f1oprswap  6862  f1o2sn  7132  residpr  7133  f1mpt  7254  f1eqcocnv  7294  isopolem  7338  3xpexg  7746  sqxpexg  7749  poxp  8127  poxp2  8142  poxp3  8149  oe0  8534  oecl  8549  nnmsucr  8637  ecopover  8835  enrefg  8998  php  9221  phpOLD  9231  3xpfi  9332  dffi3  9443  infxpenlem  10027  isfin5  10313  isfin5-2  10405  pwfseqlem4a  10675  pwfseqlem4  10676  pwfseqlem5  10677  pwfseq  10678  nqereu  10943  halfnq  10990  ltsopr  11046  1idsr  11112  00sr  11113  sqgt0sr  11120  leid  11331  msqgt0  11757  msqge0  11758  recextlem1  11867  recextlem2  11868  recex  11869  div1  11931  cju  12236  2halves  12459  msqznn  12675  xrltnr  13135  xrleid  13167  iccid  13407  m1expeven  14127  sqneg  14133  sqcl  14136  nnsqcl  14146  qsqcl  14148  expubnd  14196  bernneq  14247  faclbnd  14308  faclbnd3  14310  hashfac  14476  leiso  14477  cjmulval  15164  fallrisefac  16041  sin2t  16195  cos2t  16196  divalglem0  16412  divalglem2  16414  gcd0id  16538  lcmid  16628  lcmgcdeq  16631  lcmfsn  16654  isprm5  16726  prslem  18309  pslem  18582  dirref  18611  efmndbasabf  18850  efmndhash  18854  efmndbasfi  18855  efmnd1bas  18871  submefmnd  18873  sgrp2nmndlem4  18906  grpsubid  19007  grp1inv  19031  cntzi  19312  symgbasfi  19360  symg1bas  19372  pgrpsubgsymg  19390  symgextfve  19400  pmtrfinv  19442  psgnsn  19501  ipeq0  21598  matsca2  22358  matbas2  22359  matplusgcell  22371  matsubgcell  22372  mamulid  22379  mamurid  22380  mattposcl  22391  mat1dimelbas  22409  mat1dimscm  22413  mat1dimmul  22414  m1detdiag  22535  mdetdiagid  22538  mdetunilem9  22558  pmatcoe1fsupp  22639  d1mat2pmat  22677  idcn  23195  hausdiag  23583  symgtgp  24044  ustref  24157  ustelimasn  24161  iducn  24221  ismet  24262  isxmet  24263  idnghm  24682  resubmet  24741  xrsxmet  24749  cphnm  25145  tcphnmval  25181  ipcau2  25186  tcphcphlem1  25187  tcphcphlem2  25188  tcphcph  25189  cmssmscld  25302  chordthmlem  26794  slerflex  27727  lrrecpo  27900  subsid  28025  divs1  28159  ismot  28514  hmoval  30791  htth  30899  hvsubid  31007  hvnegid  31008  hv2times  31042  hiidrcl  31076  normval  31105  issh2  31190  chjidm  31501  normcan  31557  ho2times  31800  kbpj  31937  lnop0  31947  riesz3i  32043  leoprf  32109  leopsq  32110  cvnref  32272  gtiso  32678  fldextid  33701  prsss  33947  deranglem  35188  elfix2  35922  linedegen  36161  filnetlem2  36397  matunitlindflem2  37641  matunitlindf  37642  ftc1anclem3  37719  prdsbnd2  37819  reheibor  37863  ismgmOLD  37874  opidon2OLD  37878  exidreslem  37901  rngo2  37931  opideq  38361  eldmcoss2  38477  2xp3dxp2ge1d  42254  sn-inelr  42510  mzpf  42759  acongrep  43004  ttac  43060  mendval  43203  iocinico  43236  iocmbl  43237  seff  44333  sblpnf  44334  sigarid  46887  cnambpcma  47323  2leaddle2  47327  grlicref  48017  clintopval  48179  2arymaptfv  48631  2arymaptfo  48634  itcoval2  48644  itcoval3  48645  resipos  48949  nelsubclem  49034  initoo2  49149  termoo2  49150  setc1onsubc  49479