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  21450  1marepvsma1  22928  mdetunilem8  22964  madutpos  22987  bdayfinbndlem1  28883  ax5seg  29546  rabfodom  33173  measinblem  34923  btwnconn1lem2  37031  btwnconn1lem13  37042  athgt  40705  llnle  40767  lplnle  40789  lhpexle1  41257  lhpj1  41271  lhpat3  41295  ltrncnv  41395  cdleme16aN  41508  tendoicl  42045  cdlemk55b  42209  dihatexv  42587  dihglblem6  42589  limccog  46837  icccncfext  47102  stoweidlem31  47246  stoweidlem34  47249  stoweidlem49  47264  stoweidlem57  47272