Theorem simpll2 1021

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

Assertion

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

Proof of Theorem simpll2

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

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

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 964

This theorem is referenced by:  fidceq  6756  fidifsnen  6757  en2eqpr  6794  iunfidisj  6827  ctssdc  6991  cauappcvgprlemlol  7448  caucvgprlemlol  7471  caucvgprprlemlol  7499  elfzonelfzo  10000  qbtwnre  10027  hashun  10544  xrmaxltsup  11020  subcn2  11073  divalglemex  11608  divalglemeuneg  11609  dvdslegcd  11642  lcmledvds  11740  iscnp4  12376  cnrest2  12394  blssps  12585  blss  12586  bdbl  12661  metcnp3  12669  addcncntoplem  12709  cdivcncfap  12745