Theorem simp1ll 1253

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

Assertion

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

Proof of Theorem simp1ll

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

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1101

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 210  df-an 401  df-3an 1103

This theorem is referenced by:  lspsolvlem  21235  1marepvsma1  22701  mdetunilem8  22737  madutpos  22760  bdayfinbndlem1  28618  ax5seg  29197  rabfodom  32761  measinblem  34527  btwnconn1lem2  36451  btwnconn1lem13  36462  athgt  40092  llnle  40154  lplnle  40176  lhpexle1  40644  lhpj1  40658  lhpat3  40682  ltrncnv  40782  cdleme16aN  40895  tendoicl  41432  cdlemk55b  41596  dihatexv  41974  dihglblem6  41976  limccog  46194  icccncfext  46459  stoweidlem31  46603  stoweidlem34  46606  stoweidlem49  46621  stoweidlem57  46629