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  3243  dedth2v  3707  dedth3v  3708  dedth4v  3709  intsng  3961  complexg  4099  pw1exg  4302  ltfinirr  4457  lefinrflx  4467  0ceven  4505  evennn  4506  oddnn  4507  sucoddeven  4511  evenodddisj  4516  eventfin  4517  oddtfin  4518  nnpweq  4523  sfindbl  4530  sfintfin  4532  xpid11  4926  dfxp2  5113  brtxp  5783  elfix  5787  lecidg  6196  nncdiv3  6277  nnc3n3p1  6278  nnc3n3p2  6279  nnc3p1n3p2  6280  nchoicelem1  6289  nchoicelem2  6290