Theorem simp1ll 1233

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

Assertion

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

Proof of Theorem simp1ll

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1084

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 206  df-an 396  df-3an 1086

This theorem is referenced by:  lspsolvlem  20990  1marepvsma1  22435  mdetunilem8  22471  madutpos  22494  ax5seg  28699  rabfodom  32247  measinblem  33747  btwnconn1lem2  35592  btwnconn1lem13  35603  athgt  38839  llnle  38901  lplnle  38923  lhpexle1  39391  lhpj1  39405  lhpat3  39429  ltrncnv  39529  cdleme16aN  39642  tendoicl  40179  cdlemk55b  40343  dihatexv  40721  dihglblem6  40723  limccog  44890  icccncfext  45157  stoweidlem31  45301  stoweidlem34  45304  stoweidlem49  45319  stoweidlem57  45327