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  3852  pwnss  4132  posng  4670  sqxpexg  4714  xpid11  4821  resiexg  4923  f1mpt  5733  f1eqcocnv  5753  isopolem  5784  poxp  6191  nnmsucr  6447  erex  6516  ecopover  6590  ecopoverg  6593  enrefg  6721  3xpfi  6887  ltsopi  7252  recexnq  7322  ltsonq  7330  ltaddnq  7339  nsmallnqq  7344  ltpopr  7527  ltposr  7695  1idsr  7700  00sr  7701  axltirr  7956  leid  7973  reapirr  8466  inelr  8473  apsqgt0  8490  apirr  8494  msqge0  8505  recextlem1  8539  recexaplem2  8540  recexap  8541  div1  8590  cju  8847  2halves  9077  msqznn  9282  xrltnr  9706  xrleid  9727  iooidg  9836  iccid  9852  m1expeven  10492  expubnd  10502  sqneg  10504  sqcl  10506  sqap0  10511  nnsqcl  10514  qsqcl  10516  subsq2  10552  bernneq  10564  faclbnd  10643  faclbnd3  10645  cjmulval  10816  sin2t  11676  cos2t  11677  gcd0id  11897  lcmid  11991  lcmgcdeq  11994  idcn  12753  ismet  12885  isxmet  12886  resubmet  13089  bj-snexg  13629