Theorem simpll2 1022

Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)

Assertion

Ref	Expression
simpll2	⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜓)

Proof of Theorem simpll2

Step	Hyp	Ref	Expression
1		simpl2 986	. 2 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜓)
2	1	adantr 274	1 ⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 103   ∧ w3a 963

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106

This theorem depends on definitions:  df-bi 116  df-3an 965

This theorem is referenced by:  fidceq  6771  fidifsnen  6772  en2eqpr  6809  iunfidisj  6842  ctssdc  7006  cauappcvgprlemlol  7479  caucvgprlemlol  7502  caucvgprprlemlol  7530  elfzonelfzo  10038  qbtwnre  10065  hashun  10583  xrmaxltsup  11059  subcn2  11112  prodmodclem2  11378  divalglemex  11655  divalglemeuneg  11656  dvdslegcd  11689  lcmledvds  11787  iscnp4  12426  cnrest2  12444  blssps  12635  blss  12636  bdbl  12711  metcnp3  12719  addcncntoplem  12759  cdivcncfap  12795