Theorem anidms 383

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

Syntax hints:   → wi 4   ∧ wa 101

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

This theorem is referenced by:  sylancb  403  sylancbr  404  intsng  3674  pwnss  3937  posng  4437  xpid11m  4582  resiexg  4678  f1mpt  5435  f1eqcocnv  5456  isopolem  5486  poxp  5878  nnmsucr  6095  erex  6158  ecopover  6232  ecopoverg  6235  enrefg  6272  ltsopi  6446  recexnq  6516  ltsonq  6524  ltaddnq  6533  nsmallnqq  6538  ltpopr  6721  ltposr  6876  1idsr  6881  00sr  6882  axltirr  7115  leid  7131  reapirr  7612  inelr  7619  apsqgt0  7636  apirr  7640  msqge0  7651  recextlem1  7676  recexaplem2  7677  recexap  7678  div1  7724  cju  7959  2halves  8181  msqznn  8367  xrltnr  8772  xrleid  8791  iooidg  8849  iccid  8865  m1expeven  9432  expubnd  9442  sqneg  9444  sqcl  9446  sqap0  9451  nnsqcl  9454  qsqcl  9456  subsq2  9490  bernneq  9501  faclbnd  9573  faclbnd3  9575  cjmulval  9680  bj-snexg  10362