Theorem simpll2 1064

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

Assertion

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

Proof of Theorem simpll2

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

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

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 1007

This theorem is referenced by:  fidceq  7126  fidifsnen  7127  en2eqpr  7169  iunfidisj  7215  ctssdc  7406  cauappcvgprlemlol  7967  caucvgprlemlol  7990  caucvgprprlemlol  8018  elfzonelfzo  10582  qbtwnre  10623  nn0ltexp2  11079  hashun  11177  swrdclg  11350  xrmaxltsup  11951  subcn2  12004  prodmodclem2  12271  divalglemex  12616  divalglemeuneg  12617  dvdslegcd  12668  lcmledvds  12775  modprmn0modprm0  12962  qexpz  13058  rnglidlmcl  14677  iscnp4  15132  cnrest2  15150  blssps  15341  blss  15342  bdbl  15417  metcnp3  15425  addcncntoplem  15475  cdivcncfap  15518  lgsfcl2  15928  lgsdir  15957  lgsne0  15960  subupgr  16317  clwwlknonex2  16483