Theorem anidms 675

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 449	. 2 ⊢ (𝜑 → (𝜑 → 𝜓))
3	2	pm2.43i 50	1 ⊢ (𝜑 → 𝜓)

Syntax hints:   → wi 4   ∧ wa 383

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 196  df-an 385

This theorem is referenced by:  sylancb  696  sylancbr  697  dedth2v  4093  dedth3v  4094  dedth4v  4095  disjprsn  4196  intsng  4442  pwnss  4751  snex  4830  isso2i  4981  poinxp  5095  posn  5100  xpid11  5255  predpoirr  5611  predfrirr  5612  f1oprswap  6077  f1o2sn  6299  residpr  6300  f1mpt  6397  f1eqcocnv  6434  isopolem  6473  3xpexg  6837  sqxpexg  6839  poxp  7154  oe0  7467  oecl  7482  nnmsucr  7570  ecopover  7716  ecopoverOLD  7717  enrefg  7851  php  8007  3xpfi  8095  dffi3  8198  infxpenlem  8697  xp2cda  8863  isfin5-2  9074  fpwwe2lem5  9313  pwfseqlem4a  9340  pwfseqlem4  9341  pwfseqlem5  9342  pwfseq  9343  nqereu  9608  halfnq  9655  ltsopr  9711  1idsr  9776  00sr  9777  sqgt0sr  9784  leid  9985  msqgt0  10400  msqge0  10401  recextlem1  10509  recextlem2  10510  recex  10511  div1  10568  cju  10866  2halves  11110  msqznn  11294  xrltnr  11793  xrleid  11821  iccid  12050  m1expeven  12727  expubnd  12741  sqneg  12743  sqcl  12745  nnsqcl  12753  qsqcl  12755  subsq2  12793  bernneq  12810  faclbnd  12897  faclbnd3  12899  hashfac  13054  leiso  13055  cjmulval  13682  fallrisefac  14544  sin2t  14695  cos2t  14696  divalglem0  14903  divalglem2  14905  gcd0id  15027  lcmid  15109  lcmgcdeq  15112  lcmfsn  15135  isprm5  15206  prslem  16703  pslem  16978  dirref  17007  sgrp2nmndlem4  17187  grpsubid  17271  grp1inv  17295  cntzi  17534  symgval  17571  symgbas  17572  symgbasfi  17578  symg1bas  17588  pgrpsubgsymg  17600  symgextfve  17611  pmtrfinv  17653  psgnsn  17712  lsmidm  17849  ringadd2  18347  ipeq0  19750  matsca2  19993  matbas2  19994  matplusgcell  20006  matsubgcell  20007  mamulid  20014  mamurid  20015  mattposcl  20026  mat1dimelbas  20044  mat1dimscm  20048  mat1dimmul  20049  m1detdiag  20170  mdetdiagid  20173  mdetunilem9  20193  pmatcoe1fsupp  20273  d1mat2pmat  20311  idcn  20819  hausdiag  21206  symgtgp  21663  ustref  21780  ustelimasn  21784  iducn  21845  ismet  21886  isxmet  21887  idnghm  22305  resubmet  22361  xrsxmet  22368  cphnm  22746  tchnmval  22781  ipcau2  22786  tchcphlem1  22787  tchcphlem2  22788  tchcph  22789  chordthmlem  24304  ismot  25176  is2wlkonot  26184  is2spthonot  26185  hmoval  26843  htth  26953  hvsubid  27061  hvnegid  27062  hv2times  27096  hiidrcl  27130  normval  27159  issh2  27244  chjidm  27557  normcan  27613  ho2times  27856  kbpj  27993  lnop0  28003  riesz3i  28099  leoprf  28165  leopsq  28166  cvnref  28328  gtiso  28655  prsss  29084  deranglem  30196  dfpo2  30692  elfix2  30975  linedegen  31214  filnetlem2  31338  bj-ru0  31918  matunitlindflem2  32370  matunitlindf  32371  ftc1anclem3  32451  prdsbnd2  32558  reheibor  32602  ismgmOLD  32613  opidon2OLD  32617  exidreslem  32640  rngo2  32670  mzpf  36111  acongrep  36359  ttac  36415  mendval  36566  mendplusgfval  36568  mendmulrfval  36570  iocinico  36610  iocmbl  36611  seff  37324  sblpnf  37325  sigarid  39490  opidg  40114  cnambpcma  40158  2leaddle2  40161  clintopval  41622