Theorem simpll2 1042

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

Assertion

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

Proof of Theorem simpll2

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

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

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 985

This theorem is referenced by:  fidceq  6999  fidifsnen  7000  en2eqpr  7037  iunfidisj  7081  ctssdc  7248  cauappcvgprlemlol  7802  caucvgprlemlol  7825  caucvgprprlemlol  7853  elfzonelfzo  10403  qbtwnre  10443  nn0ltexp2  10898  hashun  10994  swrdclg  11148  xrmaxltsup  11735  subcn2  11788  prodmodclem2  12054  divalglemex  12399  divalglemeuneg  12400  dvdslegcd  12451  lcmledvds  12558  modprmn0modprm0  12745  qexpz  12841  rnglidlmcl  14409  iscnp4  14857  cnrest2  14875  blssps  15066  blss  15067  bdbl  15142  metcnp3  15150  addcncntoplem  15200  cdivcncfap  15243  lgsfcl2  15650  lgsdir  15679  lgsne0  15682