Theorem simp1ll 1238

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

Assertion

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

Proof of Theorem simp1ll

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087

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 1089

This theorem is referenced by:  lspsolvlem  21109  1marepvsma1  22539  mdetunilem8  22575  madutpos  22598  bdayfinbndlem1  28475  ax5seg  29023  rabfodom  32591  measinblem  34397  btwnconn1lem2  36301  btwnconn1lem13  36312  athgt  39826  llnle  39888  lplnle  39910  lhpexle1  40378  lhpj1  40392  lhpat3  40416  ltrncnv  40516  cdleme16aN  40629  tendoicl  41166  cdlemk55b  41330  dihatexv  41708  dihglblem6  41710  limccog  45974  icccncfext  46239  stoweidlem31  46383  stoweidlem34  46386  stoweidlem49  46401  stoweidlem57  46409