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  2128  eqeq12d  2746  rru  3753  dedth2v  4554  dedth3v  4555  dedth4v  4556  disjprsn  4681  opidg  4859  unisng  4892  intsng  4950  isso2i  5586  poinxp  5722  posn  5727  xpid11  5899  dfpo2  6272  predpoirr  6309  predfrirr  6310  f1oprswap  6847  f1o2sn  7117  residpr  7118  f1mpt  7239  f1eqcocnv  7279  isopolem  7323  3xpexg  7731  sqxpexg  7734  poxp  8110  poxp2  8125  poxp3  8132  oe0  8489  oecl  8504  nnmsucr  8592  ecopover  8797  enrefg  8958  php  9177  3xpfi  9278  dffi3  9389  infxpenlem  9973  isfin5  10259  isfin5-2  10351  pwfseqlem4a  10621  pwfseqlem4  10622  pwfseqlem5  10623  pwfseq  10624  nqereu  10889  halfnq  10936  ltsopr  10992  1idsr  11058  00sr  11059  sqgt0sr  11066  leid  11277  msqgt0  11705  msqge0  11706  recextlem1  11815  recextlem2  11816  recex  11817  div1  11879  cju  12189  2halves  12407  msqznn  12623  xrltnr  13086  xrleid  13118  iccid  13358  m1expeven  14081  sqneg  14087  sqcl  14090  nnsqcl  14100  qsqcl  14102  expubnd  14150  bernneq  14201  faclbnd  14262  faclbnd3  14264  hashfac  14430  leiso  14431  cjmulval  15118  fallrisefac  15998  sin2t  16152  cos2t  16153  divalglem0  16370  divalglem2  16372  gcd0id  16496  lcmid  16586  lcmgcdeq  16589  lcmfsn  16612  isprm5  16684  prslem  18265  pslem  18538  dirref  18567  efmndbasabf  18806  efmndhash  18810  efmndbasfi  18811  efmnd1bas  18827  submefmnd  18829  sgrp2nmndlem4  18862  grpsubid  18963  grp1inv  18987  cntzi  19268  symgbasfi  19316  symg1bas  19328  pgrpsubgsymg  19346  symgextfve  19356  pmtrfinv  19398  psgnsn  19457  ipeq0  21554  matsca2  22314  matbas2  22315  matplusgcell  22327  matsubgcell  22328  mamulid  22335  mamurid  22336  mattposcl  22347  mat1dimelbas  22365  mat1dimscm  22369  mat1dimmul  22370  m1detdiag  22491  mdetdiagid  22494  mdetunilem9  22514  pmatcoe1fsupp  22595  d1mat2pmat  22633  idcn  23151  hausdiag  23539  symgtgp  24000  ustref  24113  ustelimasn  24117  iducn  24177  ismet  24218  isxmet  24219  idnghm  24638  resubmet  24697  xrsxmet  24705  cphnm  25100  tcphnmval  25136  ipcau2  25141  tcphcphlem1  25142  tcphcphlem2  25143  tcphcph  25144  cmssmscld  25257  chordthmlem  26749  slerflex  27682  lrrecpo  27855  subsid  27980  divs1  28114  ismot  28469  hmoval  30746  htth  30854  hvsubid  30962  hvnegid  30963  hv2times  30997  hiidrcl  31031  normval  31060  issh2  31145  chjidm  31456  normcan  31512  ho2times  31755  kbpj  31892  lnop0  31902  riesz3i  31998  leoprf  32064  leopsq  32065  cvnref  32227  gtiso  32631  fldextid  33662  prsss  33913  deranglem  35160  elfix2  35899  linedegen  36138  filnetlem2  36374  matunitlindflem2  37618  matunitlindf  37619  ftc1anclem3  37696  prdsbnd2  37796  reheibor  37840  ismgmOLD  37851  opidon2OLD  37855  exidreslem  37878  rngo2  37908  opideq  38332  eldmcoss2  38457  mzpf  42731  acongrep  42976  ttac  43032  mendval  43175  iocinico  43208  iocmbl  43209  seff  44305  sblpnf  44306  sigarid  46863  cnambpcma  47299  2leaddle2  47303  grlicref  48008  clintopval  48196  2arymaptfv  48644  2arymaptfo  48647  itcoval2  48657  itcoval3  48658  resipos  48967  nelsubclem  49060  initoo2  49225  termoo2  49226  setc1onsubc  49595