Theorem simp3ll 1261

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

Assertion

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

Proof of Theorem simp3ll

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

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1101

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 210  df-an 401  df-3an 1103

This theorem is referenced by:  f1oiso2  7340  omeu  8558  ntrivcvgmul  15946  tsmsxp  24273  tgqioo  24918  ovolunlem2  25618  plyadd  26335  plymul  26336  coeeu  26343  nosupbnd1lem2  27831  noinfbnd1lem2  27846  tghilberti2  28865  btwnconn1lem2  36451  btwnconn1lem3  36452  btwnconn1lem12  36461  athgt  40092  2llnjN  40203  4atlem12b  40247  lncmp  40419  cdlema2N  40428  cdlemc2  40828  cdleme5  40876  cdleme11a  40896  cdleme21ct  40965  cdleme21  40973  cdleme22eALTN  40981  cdleme24  40988  cdleme27cl  41002  cdleme27a  41003  cdleme28  41009  cdleme36a  41096  cdleme42b  41114  cdleme48fvg  41136  cdlemf  41199  cdlemk39  41552  cdlemkid1  41558  dihlsscpre  41870  dihord4  41894  dihord5apre  41898  dihmeetlem20N  41962  mapdh9a  42425  pellex  43424  jm2.27  43597