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  20476  1marepvsma1  21804  mdetunilem8  21840  madutpos  21863  ax5seg  27415  rabfodom  30960  measinblem  32294  btwnconn1lem2  34448  btwnconn1lem13  34459  athgt  37675  llnle  37737  lplnle  37759  lhpexle1  38227  lhpj1  38241  lhpat3  38265  ltrncnv  38365  cdleme16aN  38478  tendoicl  39015  cdlemk55b  39179  dihatexv  39557  dihglblem6  39559  limccog  43398  icccncfext  43665  stoweidlem31  43809  stoweidlem34  43812  stoweidlem49  43827  stoweidlem57  43835