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

Syntax hints:   → wi 4   ∧ wa 394   ∧ 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 395  df-3an 1086

This theorem is referenced by:  lspsolvlem  21035  1marepvsma1  22503  mdetunilem8  22539  madutpos  22562  ax5seg  28767  rabfodom  32319  measinblem  33844  btwnconn1lem2  35689  btwnconn1lem13  35700  athgt  38933  llnle  38995  lplnle  39017  lhpexle1  39485  lhpj1  39499  lhpat3  39523  ltrncnv  39623  cdleme16aN  39736  tendoicl  40273  cdlemk55b  40437  dihatexv  40815  dihglblem6  40817  limccog  45010  icccncfext  45277  stoweidlem31  45421  stoweidlem34  45424  stoweidlem49  45439  stoweidlem57  45447