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  5911  f1eqcocnv  5931  isopolem  5962  poxp  6396  nnmsucr  6655  erex  6725  ecopover  6801  ecopoverg  6804  enrefg  6936  3xpfi  7125  tapeq2  7471  netap  7472  2omotaplemap  7475  ltsopi  7539  recexnq  7609  ltsonq  7617  ltaddnq  7626  nsmallnqq  7631  ltpopr  7814  ltposr  7982  1idsr  7987  00sr  7988  axltirr  8245  leid  8262  reapirr  8756  inelr  8763  apsqgt0  8780  apirr  8784  msqge0  8795  recextlem1  8830  recexaplem2  8831  recexap  8832  div1  8882  cju  9140  2halves  9372  msqznn  9579  xrltnr  10013  xrleid  10034  iooidg  10143  iccid  10159  m1expeven  10847  expubnd  10857  sqneg  10859  sqcl  10861  sqap0  10867  nnsqcl  10870  qsqcl  10872  subsq2  10908  bernneq  10921  faclbnd  11002  faclbnd3  11004  cjmulval  11448  sin2t  12309  cos2t  12310  gcd0id  12549  lcmid  12651  lcmgcdeq  12654  intopsn  13449  mgm1  13452  sgrp1  13493  mnd1  13537  mnd1id  13538  grpsubid  13666  grp1  13688  grp1inv  13689  ringadd2  14039  ring1  14071  idcn  14935  ismet  15067  isxmet  15068  resubmet  15279  bj-snexg  16507