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  21058  1marepvsma1  22476  mdetunilem8  22512  madutpos  22535  ax5seg  28871  rabfodom  32440  measinblem  34216  btwnconn1lem2  36071  btwnconn1lem13  36082  athgt  39445  llnle  39507  lplnle  39529  lhpexle1  39997  lhpj1  40011  lhpat3  40035  ltrncnv  40135  cdleme16aN  40248  tendoicl  40785  cdlemk55b  40949  dihatexv  41327  dihglblem6  41329  limccog  45611  icccncfext  45878  stoweidlem31  46022  stoweidlem34  46025  stoweidlem49  46040  stoweidlem57  46048