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  21097  1marepvsma1  22527  mdetunilem8  22563  madutpos  22586  bdayfinbndlem1  28463  ax5seg  29011  rabfodom  32580  measinblem  34377  btwnconn1lem2  36282  btwnconn1lem13  36293  athgt  39712  llnle  39774  lplnle  39796  lhpexle1  40264  lhpj1  40278  lhpat3  40302  ltrncnv  40402  cdleme16aN  40515  tendoicl  41052  cdlemk55b  41216  dihatexv  41594  dihglblem6  41596  limccog  45862  icccncfext  46127  stoweidlem31  46271  stoweidlem34  46274  stoweidlem49  46289  stoweidlem57  46297