Theorem anidms 392

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-1 5  ax-2 6  ax-mp 7  ax-ia3 107

This theorem is referenced by:  sylancb  412  sylancbr  413  intsng  3771  pwnss  4043  posng  4571  sqxpexg  4615  xpid11  4722  resiexg  4822  f1mpt  5626  f1eqcocnv  5646  isopolem  5677  poxp  6083  nnmsucr  6338  erex  6407  ecopover  6481  ecopoverg  6484  enrefg  6612  3xpfi  6772  ltsopi  7076  recexnq  7146  ltsonq  7154  ltaddnq  7163  nsmallnqq  7168  ltpopr  7351  ltposr  7506  1idsr  7511  00sr  7512  axltirr  7755  leid  7771  reapirr  8257  inelr  8264  apsqgt0  8281  apirr  8285  msqge0  8296  recextlem1  8325  recexaplem2  8326  recexap  8327  div1  8376  cju  8629  2halves  8853  msqznn  9055  xrltnr  9459  xrleid  9479  iooidg  9585  iccid  9601  m1expeven  10233  expubnd  10243  sqneg  10245  sqcl  10247  sqap0  10252  nnsqcl  10255  qsqcl  10257  subsq2  10293  bernneq  10305  faclbnd  10380  faclbnd3  10382  cjmulval  10553  sin2t  11307  cos2t  11308  gcd0id  11515  lcmid  11607  lcmgcdeq  11610  idcn  12223  ismet  12333  isxmet  12334  resubmet  12534  bj-snexg  12802