Theorem simp1ll 1232

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

Assertion

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

Proof of Theorem simp1ll

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

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  lspsolvlem  19916  1marepvsma1  21194  mdetunilem8  21230  madutpos  21253  ax5seg  26726  rabfodom  30268  measinblem  31481  btwnconn1lem2  33551  btwnconn1lem13  33562  athgt  36594  llnle  36656  lplnle  36678  lhpexle1  37146  lhpj1  37160  lhpat3  37184  ltrncnv  37284  cdleme16aN  37397  tendoicl  37934  cdlemk55b  38098  dihatexv  38476  dihglblem6  38478  limccog  41908  icccncfext  42177  stoweidlem31  42323  stoweidlem34  42326  stoweidlem49  42341  stoweidlem57  42349