Theorem anidms 678

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 52	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 197  df-an 385

This theorem is referenced by:  sylancb  700  sylancbr  701  dedth2v  4176  dedth3v  4177  dedth4v  4178  disjprsn  4282  opidg  4452  intsng  4544  pwnss  4860  snex  4938  isso2i  5096  poinxp  5216  posn  5221  xpid11  5379  predpoirr  5746  predfrirr  5747  f1oprswap  6218  f1o2sn  6448  residpr  6449  f1mpt  6558  f1eqcocnv  6596  isopolem  6635  3xpexg  7003  sqxpexg  7005  poxp  7334  oe0  7647  oecl  7662  nnmsucr  7750  ecopover  7894  enrefg  8029  php  8185  3xpfi  8273  dffi3  8378  infxpenlem  8874  xp2cda  9040  isfin5-2  9251  fpwwe2lem5  9494  pwfseqlem4a  9521  pwfseqlem4  9522  pwfseqlem5  9523  pwfseq  9524  nqereu  9789  halfnq  9836  ltsopr  9892  1idsr  9957  00sr  9958  sqgt0sr  9965  leid  10171  msqgt0  10586  msqge0  10587  recextlem1  10695  recextlem2  10696  recex  10697  div1  10754  cju  11054  2halves  11298  msqznn  11497  xrltnr  11991  xrleid  12021  iccid  12258  m1expeven  12947  expubnd  12961  sqneg  12963  sqcl  12965  nnsqcl  12973  qsqcl  12975  subsq2  13013  bernneq  13030  faclbnd  13117  faclbnd3  13119  hashfac  13280  leiso  13281  cjmulval  13929  fallrisefac  14800  sin2t  14951  cos2t  14952  divalglem0  15163  divalglem2  15165  gcd0id  15287  lcmid  15369  lcmgcdeq  15372  lcmfsn  15395  isprm5  15466  prslem  16978  pslem  17253  dirref  17282  sgrp2nmndlem4  17462  grpsubid  17546  grp1inv  17570  cntzi  17808  symgval  17845  symgbas  17846  symgbasfi  17852  symg1bas  17862  pgrpsubgsymg  17874  symgextfve  17885  pmtrfinv  17927  psgnsn  17986  lsmidm  18123  ringadd2  18621  ipeq0  20031  matsca2  20274  matbas2  20275  matplusgcell  20287  matsubgcell  20288  mamulid  20295  mamurid  20296  mattposcl  20307  mat1dimelbas  20325  mat1dimscm  20329  mat1dimmul  20330  m1detdiag  20451  mdetdiagid  20454  mdetunilem9  20474  pmatcoe1fsupp  20554  d1mat2pmat  20592  idcn  21109  hausdiag  21496  symgtgp  21952  ustref  22069  ustelimasn  22073  iducn  22134  ismet  22175  isxmet  22176  idnghm  22594  resubmet  22652  xrsxmet  22659  cphnm  23039  tchnmval  23074  ipcau2  23079  tchcphlem1  23080  tchcphlem2  23081  tchcph  23082  chordthmlem  24604  ismot  25475  hmoval  27793  htth  27903  hvsubid  28011  hvnegid  28012  hv2times  28046  hiidrcl  28080  normval  28109  issh2  28194  chjidm  28507  normcan  28563  ho2times  28806  kbpj  28943  lnop0  28953  riesz3i  29049  leoprf  29115  leopsq  29116  cvnref  29278  gtiso  29606  prsss  30090  deranglem  31274  dfpo2  31771  elfix2  32136  linedegen  32375  filnetlem2  32499  bj-ru0  33057  matunitlindflem2  33536  matunitlindf  33537  ftc1anclem3  33617  prdsbnd2  33724  reheibor  33768  ismgmOLD  33779  opidon2OLD  33783  exidreslem  33806  rngo2  33836  opideq  34250  eldmcoss2  34349  mzpf  37616  acongrep  37864  ttac  37920  mendval  38070  mendplusgfval  38072  mendmulrfval  38074  iocinico  38114  iocmbl  38115  seff  38825  sblpnf  38826  sigarid  41368  cnambpcma  41634  2leaddle2  41637  clintopval  42165