Theorem simp1ll 1237

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

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

This theorem is referenced by:  lspsolvlem  21077  1marepvsma1  22496  mdetunilem8  22532  madutpos  22555  ax5seg  28914  rabfodom  32480  measinblem  34228  btwnconn1lem2  36121  btwnconn1lem13  36132  athgt  39494  llnle  39556  lplnle  39578  lhpexle1  40046  lhpj1  40060  lhpat3  40084  ltrncnv  40184  cdleme16aN  40297  tendoicl  40834  cdlemk55b  40998  dihatexv  41376  dihglblem6  41378  limccog  45659  icccncfext  45924  stoweidlem31  46068  stoweidlem34  46071  stoweidlem49  46086  stoweidlem57  46094