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  21067  1marepvsma1  22486  mdetunilem8  22522  madutpos  22545  ax5seg  28901  rabfodom  32467  measinblem  34186  btwnconn1lem2  36061  btwnconn1lem13  36072  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  45602  icccncfext  45869  stoweidlem31  46013  stoweidlem34  46016  stoweidlem49  46031  stoweidlem57  46039