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 765	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜑)
2	1	3ad2ant1 1133	1 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) → 𝜑)

Syntax hints:   → wi 4   ∧ wa 396   ∧ 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 206  df-an 397  df-3an 1089

This theorem is referenced by:  lspsolvlem  20754  1marepvsma1  22084  mdetunilem8  22120  madutpos  22143  ax5seg  28193  rabfodom  31738  measinblem  33213  btwnconn1lem2  35055  btwnconn1lem13  35066  athgt  38322  llnle  38384  lplnle  38406  lhpexle1  38874  lhpj1  38888  lhpat3  38912  ltrncnv  39012  cdleme16aN  39125  tendoicl  39662  cdlemk55b  39826  dihatexv  40204  dihglblem6  40206  limccog  44326  icccncfext  44593  stoweidlem31  44737  stoweidlem34  44740  stoweidlem49  44755  stoweidlem57  44763