Theorem simpll2 1037

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

Assertion

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

Proof of Theorem simpll2

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

Syntax hints:   → wi 4   ∧ wa 104   ∧ w3a 978

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

This theorem depends on definitions:  df-bi 117  df-3an 980

This theorem is referenced by:  fidceq  6871  fidifsnen  6872  en2eqpr  6909  iunfidisj  6947  ctssdc  7114  cauappcvgprlemlol  7648  caucvgprlemlol  7671  caucvgprprlemlol  7699  elfzonelfzo  10232  qbtwnre  10259  nn0ltexp2  10691  hashun  10787  xrmaxltsup  11268  subcn2  11321  prodmodclem2  11587  divalglemex  11929  divalglemeuneg  11930  dvdslegcd  11967  lcmledvds  12072  modprmn0modprm0  12258  qexpz  12352  iscnp4  13803  cnrest2  13821  blssps  14012  blss  14013  bdbl  14088  metcnp3  14096  addcncntoplem  14136  cdivcncfap  14172  lgsfcl2  14492  lgsdir  14521  lgsne0  14524