Theorem simpll2 986

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

Assertion

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

Proof of Theorem simpll2

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

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

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

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

This theorem is referenced by:  fidceq  6665  fidifsnen  6666  en2eqpr  6703  iunfidisj  6735  cauappcvgprlemlol  7303  caucvgprlemlol  7326  caucvgprprlemlol  7354  elfzonelfzo  9790  qbtwnre  9817  hashun  10344  xrmaxltsup  10817  subcn2  10870  divalglemex  11364  divalglemeuneg  11365  dvdslegcd  11398  lcmledvds  11494  iscnp4  12084  cnrest2  12102  blssps  12228  blss  12229  bdbl  12304  metcnp3  12308