Theorem simp2l 1209

Description: Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.)

Assertion

Ref	Expression
simp2l	⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜓)

Proof of Theorem simp2l

Step	Hyp	Ref	Expression
1		simpl 485	. 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜓)
2	1	3ad2ant2 1143	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1095

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 399  df-3an 1097

This theorem is referenced by:  simp12l  1296  simp22l  1302  simp32l  1308  fsnunf  7154  f1oiso2  7321  fpr3g  8250  omeulem2  8536  uniinqs  8763  unxpdomlem3  9187  gruina  10762  dedekind  11332  addlid  11352  subaddmulsub  11636  dmdcan  11887  nnadddir  12255  xaddass  13238  xaddass2  13239  xlt2add  13249  xmulasslem3  13275  xadddi2  13286  xadddi2r  13287  expaddzlem  14104  expaddz  14105  expmulz  14107  expdiv  14112  expmordi  14166  modexp  14237  pfxeq  14695  ccatopth2  14716  swrdco  14836  o1add  15613  o1mul  15614  o1sub  15615  fsumsplitsnun  15754  ntrivcvgmul  15904  prmexpb  16726  pcpremul  16851  pcdiv  16860  pcqmul  16861  pcqdiv  16865  4sqlem12  16964  f1ocpbllem  17526  ercpbl  17551  erlecpbl  17552  latjlej12  18459  latmlem12  18475  latj4  18493  latj4rot  18494  gsumsgrpccat  18846  gsmsymgreqlem2  19443  symgsssg  19479  symgfisg  19480  mndodcong  19554  cmn4  19813  ablsub4  19822  abladdsub4  19823  lsm4  19872  abvdom  20848  abvres  20849  abvtrivd  20850  orngmul  20883  lspsnvs  21153  lspsneu  21162  lspfixed  21167  lspexch  21168  lsmcv  21180  lspsolvlem  21181  ring2idlqus1  21358  coe1sclmulfv  22315  matvscacell  22465  m1detdiag  22626  cramerimplem3  22714  cnprest  23318  hausnei2  23382  isreg2  23406  cmpcld  23431  llyrest  23514  nllyrest  23515  elptr  23602  basqtop  23740  hausflimlem  24008  tmdgsum  24124  utop2nei  24279  trcfilu  24322  ssblps  24451  ssbl  24452  prdsxmslem2  24558  tgqioo  24829  metnrm  24892  bndth  24989  ncvspi  25187  ncvs1  25188  cph2ass  25244  lmmbr2  25290  iscau3  25309  bcthlem5  25359  ovolunlem2  25529  dvres2  25943  dvfsumlem2  26058  plyadd  26246  plymul  26247  coeeu  26254  coemullem  26279  aalioulem4  26365  mulcxp  26716  cxplea  26727  cxple2  26728  cxplt2  26729  cxpcn3lem  26778  angcan  26833  ang180lem5  26844  divsqrtsumlem  27010  logexprlim  27255  dchrvmasumlema  27530  dchrisum0lema  27544  logdivsum  27563  log2sumbnd  27574  abvcxp  27645  padicabv  27660  nolesgn2ores  27702  nosupres  27737  nosupbnd1lem1  27738  nosupbnd1lem2  27739  nosupbnd1lem4  27741  nosupbnd1lem5  27742  nosupbnd1lem6  27743  noinffv  27751  noinfres  27752  noinfbnd1lem1  27753  noinfbnd1lem2  27754  noinfbnd1lem4  27756  noinfbnd1lem6  27758  nosupinfsep  27762  cutbdaylt  27857  expsgt0  28496  bdayfinbndlem1  28526  tghilberti2  28773  brbtwn2  29041  axcontlem4  29103  axcontlem8  29107  clwlkl1loop  29918  clwwlknonex2lem2  30245  clwlknon2num  30505  numclwlk1lem2  30507  chscllem4  31778  measxun2  34451  measun  34452  mbfmco2  34506  probun  34660  satfv1fvfmla1  35711  cgrcomim  36277  cgrcoml  36284  cgrcomr  36285  cgrdegen  36292  btwnintr  36307  btwnexch3  36308  btwnouttr2  36310  btwnouttr  36312  btwnexch  36313  btwndiff  36315  lineid  36371  idinside  36372  btwnconn1lem7  36381  btwnconn1lem8  36382  btwnconn1lem9  36383  btwnconn1lem12  36386  btwnconn1lem14  36388  btwnconn3  36391  midofsegid  36392  segcon2  36393  brsegle2  36397  btwnoutside  36413  outsideoftr  36417  outsideofeu  36419  linethru  36441  cnres2  38200  heibor  38258  lsmsat  39570  lkrlsp  39664  lkrlsp2  39665  lkrlsp3  39666  latm4  39795  omlspjN  39823  hlatj4  39936  4noncolr3  40015  4noncolr2  40016  4noncolr1  40017  athgt  40018  3dimlem3a  40022  3dimlem4a  40025  3dimlem4  40026  3dimlem4OLDN  40027  3dim3  40031  1cvratex  40035  hlatexch4  40043  3atlem4  40048  atcvrlln2  40081  atcvrlln  40082  lplnnlelln  40105  lvoli2  40143  lvolnlelln  40146  lvolnlelpln  40147  4atlem11b  40170  4atlem12b  40173  2lplnja  40181  2lplnj  40182  dalemyeo  40194  dath2  40299  lncvrat  40344  cdlemblem  40355  cdlemb  40356  elpaddri  40364  padd4N  40402  llnmod2i2  40425  llnexchb2  40431  dalawlem1  40433  dalawlem2  40434  pclfinN  40462  osumcllem6N  40523  pexmidlem3N  40534  lhp2lt  40563  lhp2at0  40594  lhp2atnle  40595  lhp2atne  40596  lhp2at0nle  40597  lhp2at0ne  40598  lhpelim  40599  lhpmod2i2  40600  lhpmod6i1  40601  lhple  40604  lhpat  40605  lhpat3  40608  ltrncoelN  40705  ltrncoat  40706  ltrncnv  40708  trlat  40731  trl0  40732  ltrnnidn  40736  trlnid  40741  cdlemd7  40766  cdleme0b  40774  cdleme0c  40775  cdleme0fN  40780  cdleme02N  40784  cdleme0ex1N  40785  cdleme0ex2N  40786  cdleme7aa  40804  cdleme7c  40807  cdleme7d  40808  cdleme7e  40809  cdleme7ga  40810  cdleme7  40811  cdleme8  40812  cdleme11a  40822  cdleme17c  40850  cdleme22gb  40856  cdlemeda  40860  cdleme20k  40881  cdleme21a  40887  cdleme21d  40892  cdleme22f2  40909  cdleme22g  40910  cdleme23a  40911  cdleme23b  40912  cdleme23c  40913  cdleme24  40914  cdleme28  40935  cdlemefrs32fva1  40963  cdlemefr32sn2aw  40966  cdlemefs32sn1aw  40976  cdleme41sn3a  40995  cdleme32fva  40999  cdleme32fva1  41000  cdleme35a  41010  cdleme35b  41012  cdleme35c  41013  cdleme35f  41016  cdleme39a  41027  cdleme42a  41033  cdleme42c  41034  cdleme42b  41040  cdleme42e  41041  cdleme42f  41042  cdleme42g  41043  cdleme42h  41044  cdleme43bN  41052  cdleme46f2g2  41055  cdleme17d2  41057  cdleme17d4  41059  cdleme48fv  41061  cdleme48fvg  41062  cdleme4gfv  41069  cdlemeg46c  41075  cdlemeg46nlpq  41079  cdlemeg46gfre  41094  cdleme48d  41097  cdlemeg49lebilem  41101  cdleme50trn2  41113  cdleme50ltrn  41119  cdleme  41122  cdlemf1  41123  cdlemf  41125  trlord  41131  ltrniotacnvval  41144  ltrniotavalbN  41146  cdlemg1cex  41150  cdlemg2dN  41152  cdlemg2ce  41154  cdlemg2fvlem  41156  cdlemg2idN  41158  cdlemg2kq  41164  cdlemg2l  41165  cdlemg2m  41166  cdlemg4b2  41172  cdlemg7fvN  41186  cdlemg8a  41189  cdlemg10bALTN  41198  cdlemg11aq  41200  cdlemg12d  41208  cdlemg13a  41213  cdlemg13  41214  cdlemg14f  41215  cdlemg14g  41216  cdlemg17a  41223  cdlemg17b  41224  cdlemg27a  41254  cdlemg31b0N  41256  cdlemg31a  41259  cdlemg31b  41260  cdlemg31c  41261  ltrnco  41281  trlcoabs  41283  trlcoabs2N  41284  trlcocnvat  41286  trlconid  41287  trlcolem  41288  trlcone  41290  cdlemg42  41291  cdlemg43  41292  cdlemg46  41297  cdlemg47  41298  tendoeq1  41326  tendoco2  41330  tendoplco2  41341  tendopltp  41342  cdlemh1  41377  cdlemh2  41378  cdlemi1  41380  cdlemi  41382  cdlemk1  41393  cdlemk2  41394  cdlemk3  41395  cdlemk4  41396  cdlemk8  41400  cdlemk9  41401  cdlemk9bN  41402  cdlemk31  41458  cdlemk32  41459  cdlemk28-3  41470  cdlemk19u  41532  cdlemk56w  41535  tendoex  41537  erngdvlem4  41553  erngdvlem4-rN  41561  dia11N  41610  dib11N  41722  cdlemn6  41764  cdlemn7  41765  cdlemn8  41766  cdlemn9  41767  dihordlem6  41775  dihordlem7  41776  dihord1  41780  dihord2a  41781  dihord2b  41782  dihord2pre  41787  dihord2pre2  41788  dihlsscpre  41796  dihvalcq2  41809  dihopelvalcpre  41810  dihord4  41820  dihord6b  41822  dihmeetlem1N  41852  dihglblem3N  41857  dihmeetlem2N  41861  dihglbcpreN  41862  dihmeetcN  41864  dihmeetbclemN  41866  dihmeetlem4preN  41868  dihjatc1  41873  dihjatc2N  41874  dihjatc3  41875  dihmeetlem9N  41877  dihmeetlem13N  41881  dihmeetlem20N  41888  dih1dimatlem0  41890  mapdpglem24  42266  mapdpglem32  42267  baerlem3lem2  42272  baerlem5alem2  42273  baerlem5blem2  42274  mapdh9aOLDN  42352  hdmap14lem6  42435  sn-addlid  42951  mzpsubst  43267  pellexlem5  43348  pellex  43350  pell14qrexpclnn0  43381  pellfundex  43401  qirropth  43423  monotuz  43456  congtr  43480  congmul  43482  congsub  43485  mzpcong  43487  fzmaxdif  43496  jm2.15nn0  43518  idomsubgmo  43708  iunrelexpmin1  44222  iunrelexpmin2  44226  trclimalb2  44240  mnringmulrcld  44742  fourierdlem42  46661  fourierdlem48  46666  fourierdlem80  46698  smfaddlem1  47275  prmdvdsfmtnof1lem1  48131  uhgrimisgrgric  48491  uspgropssxp  48704  lidldomn1  48791  rngccatidALTV  48832  coe1sclmulval  48945  lincdifsn  48984  seposep  49485  iscnrm3rlem8  49506  iscnrm3llem2  49509