Theorem anidms 397

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

Syntax hints:   → wi 4   ∧ wa 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108

This theorem is referenced by:  sylancb  418  sylancbr  419  intsng  3962  pwnss  4249  posng  4798  sqxpexg  4843  xpid11  4955  resiexg  5058  f1mpt  5912  f1eqcocnv  5932  isopolem  5963  poxp  6397  nnmsucr  6656  erex  6726  ecopover  6802  ecopoverg  6805  enrefg  6937  3xpfi  7126  tapeq2  7472  netap  7473  2omotaplemap  7476  ltsopi  7540  recexnq  7610  ltsonq  7618  ltaddnq  7627  nsmallnqq  7632  ltpopr  7815  ltposr  7983  1idsr  7988  00sr  7989  axltirr  8246  leid  8263  reapirr  8757  inelr  8764  apsqgt0  8781  apirr  8785  msqge0  8796  recextlem1  8831  recexaplem2  8832  recexap  8833  div1  8883  cju  9141  2halves  9373  msqznn  9580  xrltnr  10014  xrleid  10035  iooidg  10144  iccid  10160  m1expeven  10849  expubnd  10859  sqneg  10861  sqcl  10863  sqap0  10869  nnsqcl  10872  qsqcl  10874  subsq2  10910  bernneq  10923  faclbnd  11004  faclbnd3  11006  cjmulval  11453  sin2t  12315  cos2t  12316  gcd0id  12555  lcmid  12657  lcmgcdeq  12660  intopsn  13455  mgm1  13458  sgrp1  13499  mnd1  13543  mnd1id  13544  grpsubid  13672  grp1  13694  grp1inv  13695  ringadd2  14046  ring1  14078  idcn  14942  ismet  15074  isxmet  15075  resubmet  15286  bj-snexg  16533