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  21335  1marepvsma1  22811  mdetunilem8  22847  madutpos  22870  bdayfinbndlem1  28740  ax5seg  29403  rabfodom  32988  measinblem  34739  btwnconn1lem2  36676  btwnconn1lem13  36687  athgt  40337  llnle  40399  lplnle  40421  lhpexle1  40889  lhpj1  40903  lhpat3  40927  ltrncnv  41027  cdleme16aN  41140  tendoicl  41677  cdlemk55b  41841  dihatexv  42219  dihglblem6  42221  limccog  46458  icccncfext  46723  stoweidlem31  46867  stoweidlem34  46870  stoweidlem49  46885  stoweidlem57  46893