Theorem simp1ll 1238

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

Assertion

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

Proof of Theorem simp1ll

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087

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 1089

This theorem is referenced by:  lspsolvlem  21132  1marepvsma1  22558  mdetunilem8  22594  madutpos  22617  bdayfinbndlem1  28473  ax5seg  29021  rabfodom  32590  measinblem  34380  btwnconn1lem2  36286  btwnconn1lem13  36297  athgt  39916  llnle  39978  lplnle  40000  lhpexle1  40468  lhpj1  40482  lhpat3  40506  ltrncnv  40606  cdleme16aN  40719  tendoicl  41256  cdlemk55b  41420  dihatexv  41798  dihglblem6  41800  limccog  46068  icccncfext  46333  stoweidlem31  46477  stoweidlem34  46480  stoweidlem49  46495  stoweidlem57  46503