Theorem simpll 730

Description: Simplification of a conjunction. (Contributed by NM, 18-Mar-2007.)

Assertion

Ref	Expression
simpll	⊢ (((φ ∧ ψ) ∧ χ) → φ)

Proof of Theorem simpll

Step	Hyp	Ref	Expression
1		id 19	. 2 ⊢ (φ → φ)
2	1	ad2antrr 706	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:  simp1ll  1018  simp2ll  1022  simp3ll  1026  pm2.61da3ne  2596  rmob  3134  ifboth  3693  nndisjeq  4429  preaddccan2  4455  ltfinirr  4457  lenltfin  4469  sfintfin  4532  tfinnn  4534  imainss  5042  ncdisjun  6136  sbth  6206  leconnnc  6218  tlecg  6230  lemuc1  6253  nchoicelem4  6292  nchoicelem19  6307  nchoice  6308