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  21052  1marepvsma1  22470  mdetunilem8  22506  madutpos  22529  ax5seg  28865  rabfodom  32434  measinblem  34210  btwnconn1lem2  36076  btwnconn1lem13  36087  athgt  39450  llnle  39512  lplnle  39534  lhpexle1  40002  lhpj1  40016  lhpat3  40040  ltrncnv  40140  cdleme16aN  40253  tendoicl  40790  cdlemk55b  40954  dihatexv  41332  dihglblem6  41334  limccog  45618  icccncfext  45885  stoweidlem31  46029  stoweidlem34  46032  stoweidlem49  46047  stoweidlem57  46055