Theorem simp1ll 1249

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

Assertion

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

Proof of Theorem simp1ll

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

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1097

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 209  df-an 400  df-3an 1099

This theorem is referenced by:  lspsolvlem  21192  1marepvsma1  22623  mdetunilem8  22659  madutpos  22682  bdayfinbndlem1  28537  ax5seg  29085  rabfodom  32653  measinblem  34478  btwnconn1lem2  36402  btwnconn1lem13  36413  athgt  40044  llnle  40106  lplnle  40128  lhpexle1  40596  lhpj1  40610  lhpat3  40634  ltrncnv  40734  cdleme16aN  40847  tendoicl  41384  cdlemk55b  41548  dihatexv  41926  dihglblem6  41928  limccog  46160  icccncfext  46425  stoweidlem31  46569  stoweidlem34  46572  stoweidlem49  46587  stoweidlem57  46595