Theorem simp1ll 1238

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

Assertion

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

Proof of Theorem simp1ll

Step	Hyp	Ref	Expression
1		simpll 767	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜑)
2	1	3ad2ant1 1134	1 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) → 𝜑)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1089

This theorem is referenced by:  lspsolvlem  21140  1marepvsma1  22548  mdetunilem8  22584  madutpos  22607  bdayfinbndlem1  28459  ax5seg  29007  rabfodom  32575  measinblem  34364  btwnconn1lem2  36270  btwnconn1lem13  36281  athgt  39902  llnle  39964  lplnle  39986  lhpexle1  40454  lhpj1  40468  lhpat3  40492  ltrncnv  40592  cdleme16aN  40705  tendoicl  41242  cdlemk55b  41406  dihatexv  41784  dihglblem6  41786  limccog  46050  icccncfext  46315  stoweidlem31  46459  stoweidlem34  46462  stoweidlem49  46477  stoweidlem57  46485