Theorem simp3l 983

Description: Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.)

Assertion

Ref	Expression
simp3l	⊢ ((φ ∧ ψ ∧ (χ ∧ θ)) → χ)

Proof of Theorem simp3l

Step	Hyp	Ref	Expression
1		simpl 443	. 2 ⊢ ((χ ∧ θ) → χ)
2	1	3ad2ant3 978	1 ⊢ ((φ ∧ ψ ∧ (χ ∧ θ)) → χ)

Syntax hints:   → wi 4   ∧ wa 358   ∧ w3a 934

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  df-3an 936

This theorem is referenced by:  simpl3l  1010  simpr3l  1016  simp13l  1070  simp23l  1076  simp33l  1082  nnpw1ex  4484  tfinpw1  4494  tfinltfinlem1  4500  nnadjoin  4520  nnpweq  4523  sfin112  4529  sfindbl  4530  sfintfin  4532  sfinltfin  4535  funprgOLD  5150  fvopab4t  5385