Theorem simp1ll 1237

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

Assertion

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

Proof of Theorem simp1ll

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

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

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 1088

This theorem is referenced by:  lspsolvlem  21081  1marepvsma1  22499  mdetunilem8  22535  madutpos  22558  ax5seg  28918  rabfodom  32487  measinblem  34254  btwnconn1lem2  36153  btwnconn1lem13  36164  athgt  39575  llnle  39637  lplnle  39659  lhpexle1  40127  lhpj1  40141  lhpat3  40165  ltrncnv  40265  cdleme16aN  40378  tendoicl  40915  cdlemk55b  41079  dihatexv  41457  dihglblem6  41459  limccog  45744  icccncfext  46009  stoweidlem31  46153  stoweidlem34  46156  stoweidlem49  46171  stoweidlem57  46179