Theorem simp1ll 1236

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

Assertion

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

Proof of Theorem simp1ll

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

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

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 207  df-an 396  df-3an 1089

This theorem is referenced by:  lspsolvlem  21169  1marepvsma1  22612  mdetunilem8  22648  madutpos  22671  ax5seg  28973  rabfodom  32535  measinblem  34186  btwnconn1lem2  36054  btwnconn1lem13  36065  athgt  39415  llnle  39477  lplnle  39499  lhpexle1  39967  lhpj1  39981  lhpat3  40005  ltrncnv  40105  cdleme16aN  40218  tendoicl  40755  cdlemk55b  40919  dihatexv  41297  dihglblem6  41299  limccog  45543  icccncfext  45810  stoweidlem31  45954  stoweidlem34  45957  stoweidlem49  45972  stoweidlem57  45980