Theorem anidms 395

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

Syntax hints:   → wi 4   ∧ wa 103

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

This theorem is referenced by:  sylancb  415  sylancbr  416  intsng  3858  pwnss  4138  posng  4676  sqxpexg  4720  xpid11  4827  resiexg  4929  f1mpt  5739  f1eqcocnv  5759  isopolem  5790  poxp  6200  nnmsucr  6456  erex  6525  ecopover  6599  ecopoverg  6602  enrefg  6730  3xpfi  6896  ltsopi  7261  recexnq  7331  ltsonq  7339  ltaddnq  7348  nsmallnqq  7353  ltpopr  7536  ltposr  7704  1idsr  7709  00sr  7710  axltirr  7965  leid  7982  reapirr  8475  inelr  8482  apsqgt0  8499  apirr  8503  msqge0  8514  recextlem1  8548  recexaplem2  8549  recexap  8550  div1  8599  cju  8856  2halves  9086  msqznn  9291  xrltnr  9715  xrleid  9736  iooidg  9845  iccid  9861  m1expeven  10502  expubnd  10512  sqneg  10514  sqcl  10516  sqap0  10521  nnsqcl  10524  qsqcl  10526  subsq2  10562  bernneq  10575  faclbnd  10654  faclbnd3  10656  cjmulval  10830  sin2t  11690  cos2t  11691  gcd0id  11912  lcmid  12012  lcmgcdeq  12015  intopsn  12598  mgm1  12601  idcn  12852  ismet  12984  isxmet  12985  resubmet  13188  bj-snexg  13794