Theorem anidms 626

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 423	. 2 ⊢ (φ → (φ → ψ))
3	2	pm2.43i 43	1 ⊢ (φ → ψ)

Syntax hints:   → wi 4   ∧ wa 358

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 177  df-an 360

This theorem is referenced by:  sylancb  646  sylancbr  647  compleq  3244  dedth2v  3708  dedth3v  3709  dedth4v  3710  intsng  3962  complexg  4100  pw1exg  4303  ltfinirr  4458  lefinrflx  4468  0ceven  4506  evennn  4507  oddnn  4508  sucoddeven  4512  evenodddisj  4517  eventfin  4518  oddtfin  4519  nnpweq  4524  sfindbl  4531  sfintfin  4533  xpid11  4927  dfxp2  5114  brtxp  5784  elfix  5788  lecidg  6197  nncdiv3  6278  nnc3n3p1  6279  nnc3n3p2  6280  nnc3p1n3p2  6281  nchoicelem1  6290  nchoicelem2  6291