Theorem simp3ll 1251

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

Assertion

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

Proof of Theorem simp3ll

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1092

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 208  df-an 397  df-3an 1094

This theorem is referenced by:  f1oiso2  7297  omeu  8511  ntrivcvgmul  15859  tsmsxp  24139  tgqioo  24784  ovolunlem2  25484  plyadd  26201  plymul  26202  coeeu  26209  nosupbnd1lem2  27692  noinfbnd1lem2  27707  tghilberti2  28725  btwnconn1lem2  36325  btwnconn1lem3  36326  btwnconn1lem12  36335  athgt  39957  2llnjN  40068  4atlem12b  40112  lncmp  40284  cdlema2N  40293  cdlemc2  40693  cdleme5  40741  cdleme11a  40761  cdleme21ct  40830  cdleme21  40838  cdleme22eALTN  40846  cdleme24  40853  cdleme27cl  40867  cdleme27a  40868  cdleme28  40874  cdleme36a  40961  cdleme42b  40979  cdleme48fvg  41001  cdlemf  41064  cdlemk39  41417  cdlemkid1  41423  dihlsscpre  41735  dihord4  41759  dihord5apre  41763  dihmeetlem20N  41827  mapdh9a  42290  pellex  43289  jm2.27  43462