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

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

This theorem is referenced by:  lspsolvlem  19907  1marepvsma1  21188  mdetunilem8  21224  madutpos  21247  ax5seg  26732  rabfodom  30274  measinblem  31589  btwnconn1lem2  33662  btwnconn1lem13  33673  athgt  36752  llnle  36814  lplnle  36836  lhpexle1  37304  lhpj1  37318  lhpat3  37342  ltrncnv  37442  cdleme16aN  37555  tendoicl  38092  cdlemk55b  38256  dihatexv  38634  dihglblem6  38636  limccog  42262  icccncfext  42529  stoweidlem31  42673  stoweidlem34  42676  stoweidlem49  42691  stoweidlem57  42699