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 778	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜑)
2	1	3ad2ant1 1151	1 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) → 𝜑)

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1103

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 210  df-an 401  df-3an 1105

This theorem is referenced by:  lspsolvlem  21247  1marepvsma1  22721  mdetunilem8  22757  madutpos  22780  bdayfinbndlem1  28638  ax5seg  29266  rabfodom  32829  measinblem  34588  btwnconn1lem2  36558  btwnconn1lem13  36569  athgt  40208  llnle  40270  lplnle  40292  lhpexle1  40760  lhpj1  40774  lhpat3  40798  ltrncnv  40898  cdleme16aN  41011  tendoicl  41548  cdlemk55b  41712  dihatexv  42090  dihglblem6  42092  limccog  46316  icccncfext  46581  stoweidlem31  46725  stoweidlem34  46728  stoweidlem49  46743  stoweidlem57  46751