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  4485  tfinpw1  4495  tfinltfinlem1  4501  nnadjoin  4521  nnpweq  4524  sfin112  4530  sfindbl  4531  sfintfin  4533  sfinltfin  4536  funprgOLD  5151  fvopab4t  5386