Theorem simp3ll 1257

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

Assertion

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

Proof of Theorem simp3ll

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

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1097

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 209  df-an 400  df-3an 1099

This theorem is referenced by:  f1oiso2  7332  omeu  8549  ntrivcvgmul  15915  tsmsxp  24195  tgqioo  24840  ovolunlem2  25540  plyadd  26257  plymul  26258  coeeu  26265  nosupbnd1lem2  27750  noinfbnd1lem2  27765  tghilberti2  28784  btwnconn1lem2  36402  btwnconn1lem3  36403  btwnconn1lem12  36412  athgt  40044  2llnjN  40155  4atlem12b  40199  lncmp  40371  cdlema2N  40380  cdlemc2  40780  cdleme5  40828  cdleme11a  40848  cdleme21ct  40917  cdleme21  40925  cdleme22eALTN  40933  cdleme24  40940  cdleme27cl  40954  cdleme27a  40955  cdleme28  40961  cdleme36a  41048  cdleme42b  41066  cdleme48fvg  41088  cdlemf  41151  cdlemk39  41504  cdlemkid1  41510  dihlsscpre  41822  dihord4  41846  dihord5apre  41850  dihmeetlem20N  41914  mapdh9a  42377  pellex  43376  jm2.27  43549