Theorem simp3ll 1245

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 1135	1 ⊢ ((𝜃 ∧ 𝜏 ∧ ((𝜑 ∧ 𝜓) ∧ 𝜒)) → 𝜑)

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

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 207  df-an 396  df-3an 1088

This theorem is referenced by:  f1oiso2  7286  omeu  8500  ntrivcvgmul  15806  tsmsxp  24068  tgqioo  24713  ovolunlem2  25424  plyadd  26147  plymul  26148  coeeu  26155  nosupbnd1lem2  27646  noinfbnd1lem2  27661  tghilberti2  28614  btwnconn1lem2  36121  btwnconn1lem3  36122  btwnconn1lem12  36131  athgt  39494  2llnjN  39605  4atlem12b  39649  lncmp  39821  cdlema2N  39830  cdlemc2  40230  cdleme5  40278  cdleme11a  40298  cdleme21ct  40367  cdleme21  40375  cdleme22eALTN  40383  cdleme24  40390  cdleme27cl  40404  cdleme27a  40405  cdleme28  40411  cdleme36a  40498  cdleme42b  40516  cdleme48fvg  40538  cdlemf  40601  cdlemk39  40954  cdlemkid1  40960  dihlsscpre  41272  dihord4  41296  dihord5apre  41300  dihmeetlem20N  41364  mapdh9a  41827  pellex  42867  jm2.27  43040