Theorem simp1ll 1254

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 1150	1 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) → 𝜑)

This proof depends on syntax axioms:   → wi 4   ∧ wa 400   ∧ w3a 1102

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

This theorem is used by:  lspsolvlem  21277  1marepvsma1  22751  mdetunilem8  22787  madutpos  22810  bdayfinbndlem1  28671  ax5seg  29299  rabfodom  32862  measinblem  34619  btwnconn1lem2  36588  btwnconn1lem13  36599  athgt  40258  llnle  40320  lplnle  40342  lhpexle1  40810  lhpj1  40824  lhpat3  40848  ltrncnv  40948  cdleme16aN  41061  tendoicl  41598  cdlemk55b  41762  dihatexv  42140  dihglblem6  42142  limccog  46364  icccncfext  46629  stoweidlem31  46773  stoweidlem34  46776  stoweidlem49  46791  stoweidlem57  46799