Theorem simp1ll 1255

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

Assertion

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

Proof of Theorem simp1ll

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  lspsolvlem  21400  1marepvsma1  22878  mdetunilem8  22914  madutpos  22937  bdayfinbndlem1  28835  ax5seg  29498  rabfodom  33083  measinblem  34835  btwnconn1lem2  36823  btwnconn1lem13  36834  athgt  40481  llnle  40543  lplnle  40565  lhpexle1  41033  lhpj1  41047  lhpat3  41071  ltrncnv  41171  cdleme16aN  41284  tendoicl  41821  cdlemk55b  41985  dihatexv  42363  dihglblem6  42365  limccog  46576  icccncfext  46841  stoweidlem31  46985  stoweidlem34  46988  stoweidlem49  47003  stoweidlem57  47011