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  6863  fidifsnen  6864  en2eqpr  6901  iunfidisj  6939  ctssdc  7106  cauappcvgprlemlol  7637  caucvgprlemlol  7660  caucvgprprlemlol  7688  elfzonelfzo  10216  qbtwnre  10243  nn0ltexp2  10674  hashun  10769  xrmaxltsup  11250  subcn2  11303  prodmodclem2  11569  divalglemex  11910  divalglemeuneg  11911  dvdslegcd  11948  lcmledvds  12053  modprmn0modprm0  12239  qexpz  12333  iscnp4  13385  cnrest2  13403  blssps  13594  blss  13595  bdbl  13670  metcnp3  13678  addcncntoplem  13718  cdivcncfap  13754  lgsfcl2  14074  lgsdir  14103  lgsne0  14106