Theorem simp3ll 1242

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

Assertion

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

Proof of Theorem simp3ll

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1085

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 206  df-an 396  df-3an 1087

This theorem is referenced by:  f1oiso2  7354  omeu  8599  ntrivcvgmul  15874  tsmsxp  24052  tgqioo  24709  ovolunlem2  25420  plyadd  26144  plymul  26145  coeeu  26152  nosupbnd1lem2  27635  noinfbnd1lem2  27650  tghilberti2  28435  btwnconn1lem2  35674  btwnconn1lem3  35675  btwnconn1lem12  35684  athgt  38918  2llnjN  39029  4atlem12b  39073  lncmp  39245  cdlema2N  39254  cdlemc2  39654  cdleme5  39702  cdleme11a  39722  cdleme21ct  39791  cdleme21  39799  cdleme22eALTN  39807  cdleme24  39814  cdleme27cl  39828  cdleme27a  39829  cdleme28  39835  cdleme36a  39922  cdleme42b  39940  cdleme48fvg  39962  cdlemf  40025  cdlemk39  40378  cdlemkid1  40384  dihlsscpre  40696  dihord4  40720  dihord5apre  40724  dihmeetlem20N  40788  mapdh9a  41251  pellex  42227  jm2.27  42401