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  21425  1marepvsma1  22903  mdetunilem8  22939  madutpos  22962  bdayfinbndlem1  28858  ax5seg  29521  rabfodom  33148  measinblem  34899  btwnconn1lem2  36945  btwnconn1lem13  36956  athgt  40606  llnle  40668  lplnle  40690  lhpexle1  41158  lhpj1  41172  lhpat3  41196  ltrncnv  41296  cdleme16aN  41409  tendoicl  41946  cdlemk55b  42110  dihatexv  42488  dihglblem6  42490  limccog  46725  icccncfext  46990  stoweidlem31  47134  stoweidlem34  47137  stoweidlem49  47152  stoweidlem57  47160