Theorem simpll2 1040

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

Assertion

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

Proof of Theorem simpll2

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

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

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 983

This theorem is referenced by:  fidceq  6973  fidifsnen  6974  en2eqpr  7011  iunfidisj  7055  ctssdc  7222  cauappcvgprlemlol  7767  caucvgprlemlol  7790  caucvgprprlemlol  7818  elfzonelfzo  10366  qbtwnre  10406  nn0ltexp2  10861  hashun  10957  swrdclg  11111  xrmaxltsup  11613  subcn2  11666  prodmodclem2  11932  divalglemex  12277  divalglemeuneg  12278  dvdslegcd  12329  lcmledvds  12436  modprmn0modprm0  12623  qexpz  12719  rnglidlmcl  14286  iscnp4  14734  cnrest2  14752  blssps  14943  blss  14944  bdbl  15019  metcnp3  15027  addcncntoplem  15077  cdivcncfap  15120  lgsfcl2  15527  lgsdir  15556  lgsne0  15559