Theorem simp1ll 1235

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

Assertion

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

Proof of Theorem simp1ll

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1086

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 1088

This theorem is referenced by:  lspsolvlem  20404  1marepvsma1  21732  mdetunilem8  21768  madutpos  21791  ax5seg  27306  rabfodom  30851  measinblem  32188  btwnconn1lem2  34390  btwnconn1lem13  34401  athgt  37470  llnle  37532  lplnle  37554  lhpexle1  38022  lhpj1  38036  lhpat3  38060  ltrncnv  38160  cdleme16aN  38273  tendoicl  38810  cdlemk55b  38974  dihatexv  39352  dihglblem6  39354  limccog  43161  icccncfext  43428  stoweidlem31  43572  stoweidlem34  43575  stoweidlem49  43590  stoweidlem57  43598