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  2752  rru  3725  dedth2v  4529  dedth3v  4530  dedth4v  4531  disjprsn  4658  opidg  4835  unisng  4868  intsng  4925  isso2i  5576  poinxp  5712  posn  5717  xpid11  5887  dfpo2  6260  predpoirr  6297  predfrirr  6298  f1oprswap  6825  f1o2sn  7095  residpr  7096  f1mpt  7216  f1eqcocnv  7256  isopolem  7300  3xpexg  7706  sqxpexg  7709  poxp  8078  poxp2  8093  poxp3  8100  oe0  8457  oecl  8472  nnmsucr  8561  ecopover  8768  enrefg  8931  php  9141  3xpfi  9231  dffi3  9344  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  11242  msqgt0  11670  msqge0  11671  recextlem1  11780  recextlem2  11781  recex  11782  div1  11844  cju  12155  2halves  12395  msqznn  12611  xrltnr  13070  xrleid  13102  iccid  13343  m1expeven  14071  sqneg  14077  sqcl  14080  nnsqcl  14090  qsqcl  14092  expubnd  14140  bernneq  14191  faclbnd  14252  faclbnd3  14254  hashfac  14420  leiso  14421  cjmulval  15107  fallrisefac  15990  sin2t  16144  cos2t  16145  divalglem0  16362  divalglem2  16364  gcd0id  16488  lcmid  16578  lcmgcdeq  16581  lcmfsn  16604  isprm5  16677  prslem  18263  pslem  18538  dirref  18567  efmndbasabf  18840  efmndhash  18844  efmndbasfi  18845  efmnd1bas  18861  submefmnd  18863  sgrp2nmndlem4  18899  grpsubid  19000  grp1inv  19024  cntzi  19304  symgbasfi  19354  symg1bas  19366  pgrpsubgsymg  19384  symgextfve  19394  pmtrfinv  19436  psgnsn  19495  ipeq0  21618  matsca2  22385  matbas2  22386  matplusgcell  22398  matsubgcell  22399  mamulid  22406  mamurid  22407  mattposcl  22418  mat1dimelbas  22436  mat1dimscm  22440  mat1dimmul  22441  m1detdiag  22562  mdetdiagid  22565  mdetunilem9  22585  pmatcoe1fsupp  22666  d1mat2pmat  22704  idcn  23222  hausdiag  23610  symgtgp  24071  ustref  24184  ustelimasn  24188  iducn  24247  ismet  24288  isxmet  24289  idnghm  24708  resubmet  24767  xrsxmet  24775  cphnm  25160  tcphnmval  25196  ipcau2  25201  tcphcphlem1  25202  tcphcphlem2  25203  tcphcph  25204  cmssmscld  25317  chordthmlem  26796  lesid  27731  lrrecpo  27933  subsid  28061  divs1  28196  zsoring  28401  ismot  28603  hmoval  30881  htth  30989  hvsubid  31097  hvnegid  31098  hv2times  31132  hiidrcl  31166  normval  31195  issh2  31280  chjidm  31591  normcan  31647  ho2times  31890  kbpj  32027  lnop0  32037  riesz3i  32133  leoprf  32199  leopsq  32200  cvnref  32362  gtiso  32774  fldextid  33803  prsss  34060  fineqvnttrclse  35268  deranglem  35348  elfix2  36084  linedegen  36325  filnetlem2  36561  matunitlindflem2  37938  matunitlindf  37939  ftc1anclem3  38016  prdsbnd2  38116  reheibor  38160  ismgmOLD  38171  opidon2OLD  38175  exidreslem  38198  rngo2  38228  opideq  38664  eldmcoss2  38870  mzpf  43168  acongrep  43408  ttac  43464  mendval  43607  iocinico  43640  iocmbl  43641  seff  44736  sblpnf  44737  sigarid  47286  cnambpcma  47742  2leaddle2  47746  grlicref  48488  clintopval  48680  2arymaptfv  49127  2arymaptfo  49130  itcoval2  49140  itcoval3  49141  resipos  49450  nelsubclem  49542  initoo2  49707  termoo2  49708  setc1onsubc  50077