Theorem simp1ll 1234

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

Assertion

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

Proof of Theorem simp1ll

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

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

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 206  df-an 396  df-3an 1087

This theorem is referenced by:  lspsolvlem  20319  1marepvsma1  21640  mdetunilem8  21676  madutpos  21699  ax5seg  27209  rabfodom  30752  measinblem  32088  btwnconn1lem2  34317  btwnconn1lem13  34328  athgt  37397  llnle  37459  lplnle  37481  lhpexle1  37949  lhpj1  37963  lhpat3  37987  ltrncnv  38087  cdleme16aN  38200  tendoicl  38737  cdlemk55b  38901  dihatexv  39279  dihglblem6  39281  limccog  43051  icccncfext  43318  stoweidlem31  43462  stoweidlem34  43465  stoweidlem49  43480  stoweidlem57  43488