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  21049  1marepvsma1  22468  mdetunilem8  22504  madutpos  22527  ax5seg  28883  rabfodom  32449  measinblem  34187  btwnconn1lem2  36062  btwnconn1lem13  36073  athgt  39435  llnle  39497  lplnle  39519  lhpexle1  39987  lhpj1  40001  lhpat3  40025  ltrncnv  40125  cdleme16aN  40238  tendoicl  40775  cdlemk55b  40939  dihatexv  41317  dihglblem6  41319  limccog  45601  icccncfext  45868  stoweidlem31  46012  stoweidlem34  46015  stoweidlem49  46030  stoweidlem57  46038