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  2749  rru  3734  dedth2v  4539  dedth3v  4540  dedth4v  4541  disjprsn  4668  opidg  4845  unisng  4878  intsng  4935  isso2i  5566  poinxp  5702  posn  5707  xpid11  5878  dfpo2  6250  predpoirr  6287  predfrirr  6288  f1oprswap  6815  f1o2sn  7083  residpr  7084  f1mpt  7203  f1eqcocnv  7243  isopolem  7287  3xpexg  7693  sqxpexg  7696  poxp  8066  poxp2  8081  poxp3  8088  oe0  8445  oecl  8460  nnmsucr  8548  ecopover  8753  enrefg  8915  php  9125  3xpfi  9214  dffi3  9324  infxpenlem  9913  isfin5  10199  isfin5-2  10291  pwfseqlem4a  10561  pwfseqlem4  10562  pwfseqlem5  10563  pwfseq  10564  nqereu  10829  halfnq  10876  ltsopr  10932  1idsr  10998  00sr  10999  sqgt0sr  11006  leid  11218  msqgt0  11646  msqge0  11647  recextlem1  11756  recextlem2  11757  recex  11758  div1  11820  cju  12130  2halves  12348  msqznn  12563  xrltnr  13022  xrleid  13054  iccid  13294  m1expeven  14020  sqneg  14026  sqcl  14029  nnsqcl  14039  qsqcl  14041  expubnd  14089  bernneq  14140  faclbnd  14201  faclbnd3  14203  hashfac  14369  leiso  14370  cjmulval  15056  fallrisefac  15936  sin2t  16090  cos2t  16091  divalglem0  16308  divalglem2  16310  gcd0id  16434  lcmid  16524  lcmgcdeq  16527  lcmfsn  16550  isprm5  16622  prslem  18207  pslem  18482  dirref  18511  efmndbasabf  18784  efmndhash  18788  efmndbasfi  18789  efmnd1bas  18805  submefmnd  18807  sgrp2nmndlem4  18840  grpsubid  18941  grp1inv  18965  cntzi  19245  symgbasfi  19295  symg1bas  19307  pgrpsubgsymg  19325  symgextfve  19335  pmtrfinv  19377  psgnsn  19436  ipeq0  21579  matsca2  22338  matbas2  22339  matplusgcell  22351  matsubgcell  22352  mamulid  22359  mamurid  22360  mattposcl  22371  mat1dimelbas  22389  mat1dimscm  22393  mat1dimmul  22394  m1detdiag  22515  mdetdiagid  22518  mdetunilem9  22538  pmatcoe1fsupp  22619  d1mat2pmat  22657  idcn  23175  hausdiag  23563  symgtgp  24024  ustref  24137  ustelimasn  24141  iducn  24200  ismet  24241  isxmet  24242  idnghm  24661  resubmet  24720  xrsxmet  24728  cphnm  25123  tcphnmval  25159  ipcau2  25164  tcphcphlem1  25165  tcphcphlem2  25166  tcphcph  25167  cmssmscld  25280  chordthmlem  26772  slerflex  27705  lrrecpo  27887  subsid  28012  divs1  28146  zsoring  28335  ismot  28516  hmoval  30794  htth  30902  hvsubid  31010  hvnegid  31011  hv2times  31045  hiidrcl  31079  normval  31108  issh2  31193  chjidm  31504  normcan  31560  ho2times  31803  kbpj  31940  lnop0  31950  riesz3i  32046  leoprf  32112  leopsq  32113  cvnref  32275  gtiso  32688  fldextid  33695  prsss  33952  fineqvnttrclse  35167  deranglem  35233  elfix2  35969  linedegen  36210  filnetlem2  36446  matunitlindflem2  37680  matunitlindf  37681  ftc1anclem3  37758  prdsbnd2  37858  reheibor  37902  ismgmOLD  37913  opidon2OLD  37917  exidreslem  37940  rngo2  37970  opideq  38398  eldmcoss2  38584  mzpf  42856  acongrep  43100  ttac  43156  mendval  43299  iocinico  43332  iocmbl  43333  seff  44429  sblpnf  44430  sigarid  46983  cnambpcma  47421  2leaddle2  47425  grlicref  48139  clintopval  48331  2arymaptfv  48779  2arymaptfo  48782  itcoval2  48792  itcoval3  48793  resipos  49102  nelsubclem  49195  initoo2  49360  termoo2  49361  setc1onsubc  49730