Theorem simp1ll 1255

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

Assertion

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

Proof of Theorem simp1ll

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  lspsolvlem  21303  1marepvsma1  22777  mdetunilem8  22813  madutpos  22836  bdayfinbndlem1  28697  ax5seg  29325  rabfodom  32888  measinblem  34642  btwnconn1lem2  36601  btwnconn1lem13  36612  athgt  40271  llnle  40333  lplnle  40355  lhpexle1  40823  lhpj1  40837  lhpat3  40861  ltrncnv  40961  cdleme16aN  41074  tendoicl  41611  cdlemk55b  41775  dihatexv  42153  dihglblem6  42155  limccog  46377  icccncfext  46642  stoweidlem31  46786  stoweidlem34  46789  stoweidlem49  46804  stoweidlem57  46812