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  2132  eqeq12d  2752  rru  3737  dedth2v  4542  dedth3v  4543  dedth4v  4544  disjprsn  4671  opidg  4848  unisng  4881  intsng  4938  isso2i  5569  poinxp  5705  posn  5710  xpid11  5881  dfpo2  6254  predpoirr  6291  predfrirr  6292  f1oprswap  6819  f1o2sn  7087  residpr  7088  f1mpt  7207  f1eqcocnv  7247  isopolem  7291  3xpexg  7697  sqxpexg  7700  poxp  8070  poxp2  8085  poxp3  8092  oe0  8449  oecl  8464  nnmsucr  8553  ecopover  8758  enrefg  8921  php  9131  3xpfi  9221  dffi3  9334  infxpenlem  9923  isfin5  10209  isfin5-2  10301  pwfseqlem4a  10572  pwfseqlem4  10573  pwfseqlem5  10574  pwfseq  10575  nqereu  10840  halfnq  10887  ltsopr  10943  1idsr  11009  00sr  11010  sqgt0sr  11017  leid  11229  msqgt0  11657  msqge0  11658  recextlem1  11767  recextlem2  11768  recex  11769  div1  11831  cju  12141  2halves  12359  msqznn  12574  xrltnr  13033  xrleid  13065  iccid  13306  m1expeven  14032  sqneg  14038  sqcl  14041  nnsqcl  14051  qsqcl  14053  expubnd  14101  bernneq  14152  faclbnd  14213  faclbnd3  14215  hashfac  14381  leiso  14382  cjmulval  15068  fallrisefac  15948  sin2t  16102  cos2t  16103  divalglem0  16320  divalglem2  16322  gcd0id  16446  lcmid  16536  lcmgcdeq  16539  lcmfsn  16562  isprm5  16634  prslem  18220  pslem  18495  dirref  18524  efmndbasabf  18797  efmndhash  18801  efmndbasfi  18802  efmnd1bas  18818  submefmnd  18820  sgrp2nmndlem4  18853  grpsubid  18954  grp1inv  18978  cntzi  19258  symgbasfi  19308  symg1bas  19320  pgrpsubgsymg  19338  symgextfve  19348  pmtrfinv  19390  psgnsn  19449  ipeq0  21593  matsca2  22364  matbas2  22365  matplusgcell  22377  matsubgcell  22378  mamulid  22385  mamurid  22386  mattposcl  22397  mat1dimelbas  22415  mat1dimscm  22419  mat1dimmul  22420  m1detdiag  22541  mdetdiagid  22544  mdetunilem9  22564  pmatcoe1fsupp  22645  d1mat2pmat  22683  idcn  23201  hausdiag  23589  symgtgp  24050  ustref  24163  ustelimasn  24167  iducn  24226  ismet  24267  isxmet  24268  idnghm  24687  resubmet  24746  xrsxmet  24754  cphnm  25149  tcphnmval  25185  ipcau2  25190  tcphcphlem1  25191  tcphcphlem2  25192  tcphcph  25193  cmssmscld  25306  chordthmlem  26798  lesid  27735  lrrecpo  27937  subsid  28065  divs1  28200  zsoring  28405  ismot  28607  hmoval  30885  htth  30993  hvsubid  31101  hvnegid  31102  hv2times  31136  hiidrcl  31170  normval  31199  issh2  31284  chjidm  31595  normcan  31651  ho2times  31894  kbpj  32031  lnop0  32041  riesz3i  32137  leoprf  32203  leopsq  32204  cvnref  32366  gtiso  32780  fldextid  33816  prsss  34073  fineqvnttrclse  35280  deranglem  35360  elfix2  36096  linedegen  36337  filnetlem2  36573  matunitlindflem2  37818  matunitlindf  37819  ftc1anclem3  37896  prdsbnd2  37996  reheibor  38040  ismgmOLD  38051  opidon2OLD  38055  exidreslem  38078  rngo2  38108  opideq  38536  eldmcoss2  38722  mzpf  42978  acongrep  43222  ttac  43278  mendval  43421  iocinico  43454  iocmbl  43455  seff  44550  sblpnf  44551  sigarid  47102  cnambpcma  47540  2leaddle2  47544  grlicref  48258  clintopval  48450  2arymaptfv  48897  2arymaptfo  48900  itcoval2  48910  itcoval3  48911  resipos  49220  nelsubclem  49312  initoo2  49477  termoo2  49478  setc1onsubc  49847