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 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  21171  1marepvsma1  22614  mdetunilem8  22650  madutpos  22673  ax5seg  28979  rabfodom  32548  measinblem  34215  btwnconn1lem2  36083  btwnconn1lem13  36094  athgt  39453  llnle  39515  lplnle  39537  lhpexle1  40005  lhpj1  40019  lhpat3  40043  ltrncnv  40143  cdleme16aN  40256  tendoicl  40793  cdlemk55b  40957  dihatexv  41335  dihglblem6  41337  limccog  45604  icccncfext  45871  stoweidlem31  46015  stoweidlem34  46018  stoweidlem49  46033  stoweidlem57  46041