Theorem simp2r 1210

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

Assertion

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

Proof of Theorem simp2r

Step	Hyp	Ref	Expression
1		simpr 487	. 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:  simp12r  1297  simp22r  1303  simp32r  1309  fsnunf  7154  f1oiso2  7321  fnsuppres  8155  frrlem4  8254  omeulem2  8536  uniinqs  8763  unxpdomlem3  9187  sup0  9399  fin23lem11  10260  reclem3pr  10993  dedekind  11332  addlid  11352  subaddmulsub  11636  dmdcan  11887  nnadddir  12255  xaddass2  13239  xlt2add  13249  xadddi2  13286  expaddzlem  14104  expaddz  14105  expmulz  14107  expdiv  14112  expmordi  14166  pfxeq  14695  ccatopth2  14716  relexpaddnn  15050  o1add  15613  o1mul  15614  o1sub  15615  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  gsumsgrpccat  18846  symgsssg  19479  symgfisg  19480  mndodcong  19554  cmn4  19813  ablsub4  19822  abladdsub4  19823  lsm4  19872  abvdom  20848  abvtrivd  20850  orngmul  20883  lspsnvs  21153  lspsneu  21162  lspfixed  21167  lspexch  21168  lsmcv  21180  lspsolvlem  21181  mvrf1  22006  coe1sclmulfv  22315  m1detdiag  22626  cnprest  23318  isreg2  23406  elptr  23602  hausflimlem  24008  trcfilu  24322  ssblps  24451  ssbl  24452  prdsxmslem2  24558  tgqioo  24829  metnrm  24892  bndth  24989  ncvspi  25187  cph2ass  25244  iscau3  25309  ovolunlem2  25529  dvres2  25943  dvfsumlem2  26058  dvfsum2  26065  deg1tm  26148  plyadd  26246  plymul  26247  coeeu  26254  coemullem  26279  aalioulem4  26365  cxplea  26727  cxple2  26728  cxplt2  26729  cxple2a  26730  cxpcn3lem  26778  angcan  26833  ang180lem5  26844  divsqrtsumlem  27010  logexprlim  27255  dchrvmasumlema  27530  dchrisum0lema  27544  logdivsum  27563  log2sumbnd  27574  padicabv  27660  nolesgn2ores  27702  nogesgn1o  27703  nogesgn1ores  27704  nolt02o  27725  nogt01o  27726  nosupinfsep  27762  noetalem1  27771  noeta2  27820  cutbdaylt  27857  expsgt0  28496  bdayfinbndlem1  28526  tghilberti2  28773  brbtwn2  29041  axcontlem4  29103  axcontlem8  29107  clwlkl1loop  29918  chscllem4  31778  mdslmd4i  32471  nexple  32985  measxun2  34451  measun  34452  mbfmco2  34506  probun  34660  satfv1fvfmla1  35711  wsuclem  36111  cgrcomim  36277  cgrcoml  36284  cgrcomr  36285  cgrdegen  36292  btwnintr  36307  btwnexch3  36308  btwnouttr  36312  btwnexch  36313  btwndiff  36315  ifscgr  36332  lineid  36371  btwnconn1lem7  36381  btwnconn1lem8  36382  btwnconn1lem9  36383  btwnconn1lem12  36386  midofsegid  36392  brsegle2  36397  btwnoutside  36413  outsideoftr  36417  ttcmin  36794  cnres2  38200  heibor  38258  lsmsat  39570  lkrlsp  39664  lkrlsp2  39665  lkrlsp3  39666  lshpkrlem6  39677  latm4  39795  omlspjN  39823  hlatj4  39936  4noncolr3  40015  4noncolr2  40016  4noncolr1  40017  3dimlem3a  40022  3dimlem4a  40025  3dimlem4  40026  3dimlem4OLDN  40027  1cvratex  40035  hlatexch4  40043  3atlem4  40048  atcvrlln2  40081  atcvrlln  40082  llnmlplnN  40101  lplnnlelln  40105  lvoli2  40143  lvolnlelln  40146  lvolnlelpln  40147  4atlem11b  40170  4atlem12b  40173  2lplnj  40182  dalemzeo  40195  dath2  40299  lncvrat  40344  cdlemb  40356  elpaddri  40364  padd4N  40402  llnmod2i2  40425  llnexchb2  40431  dalawlem1  40433  dalawlem2  40434  osumcllem6N  40523  pexmidlem3N  40534  pexmidlem4N  40535  lhp2lt  40563  lhp2at0  40594  lhp2atne  40596  lhp2at0ne  40598  lhpmod2i2  40600  lhpmod6i1  40601  lhpat  40605  lhpat3  40608  4atexlemex6  40636  ltrncoval  40707  ltrncnv  40708  ltrnnidn  40736  cdlemd7  40766  cdleme0b  40774  cdleme0c  40775  cdleme0fN  40780  cdleme0ex1N  40785  cdleme7d  40808  cdleme7e  40809  cdleme7ga  40810  cdleme7  40811  cdleme11a  40822  cdleme17c  40850  cdleme22gb  40856  cdlemeda  40860  cdleme20k  40881  cdleme21a  40887  cdleme21at  40890  cdleme21d  40892  cdleme22f2  40909  cdleme22g  40910  cdleme24  40914  cdleme28  40935  cdlemefrs29cpre1  40960  cdlemefr29exN  40964  cdlemefr32sn2aw  40966  cdleme32fva  40999  cdleme32fva1  41000  cdleme35a  41010  cdleme42c  41034  cdleme42e  41041  cdleme42f  41042  cdleme42g  41043  cdleme42h  41044  cdleme43bN  41052  cdleme46f2g2  41055  cdleme17d2  41057  cdleme4gfv  41069  cdlemeg46c  41075  cdlemeg46nlpq  41079  cdlemeg46gfre  41094  cdlemeg49lebilem  41101  cdleme50trn1  41111  cdleme50trn2  41113  cdleme50ltrn  41119  cdleme  41122  cdlemf1  41123  cdlemf  41125  trlord  41131  ltrniotavalbN  41146  cdlemg1cex  41150  cdlemg2dN  41152  cdlemg2ce  41154  cdlemg2fvlem  41156  cdlemg2idN  41158  cdlemg2kq  41164  cdlemg2l  41165  cdlemg7fvN  41186  cdlemg7aN  41187  cdlemg8a  41189  cdlemg11aq  41200  cdlemg12d  41208  cdlemg13a  41213  cdlemg13  41214  cdlemg14f  41215  cdlemg14g  41216  cdlemg17b  41224  cdlemg27a  41254  cdlemg31b0N  41256  cdlemg31a  41259  cdlemg31b  41260  cdlemg31c  41261  ltrnco  41281  trlcoabs2N  41284  trlcocnvat  41286  trlconid  41287  trlcolem  41288  cdlemg42  41291  cdlemg43  41292  cdlemg47a  41296  cdlemg46  41297  cdlemg47  41298  tendoeq1  41326  tendocoval  41328  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  cdlemk28-3  41470  cdlemk19xlem  41504  cdlemk39u  41530  cdlemk19u  41532  cdlemk56w  41535  cdlemn7  41765  cdlemn8  41766  cdlemn9  41767  dihordlem6  41775  dihordlem7  41776  dihordlem7b  41777  dihord1  41780  dihord2a  41781  dihord11c  41786  dihord2pre  41787  dihord2pre2  41788  dihlsscpre  41796  dihord4  41820  dihord6b  41822  dihmeetlem2N  41861  dihglbcpreN  41862  dihmeetcN  41864  dihmeetbclemN  41866  dihmeetlem3N  41867  dihmeetlem9N  41877  dihmeetlem13N  41881  dihmeetlem20N  41888  mapdpglem24  42266  mapdpglem32  42267  baerlem3lem2  42272  baerlem5alem2  42273  baerlem5blem2  42274  mapdh9aOLDN  42352  hdmap14lem6  42435  sn-addlid  42951  mzpmfp  43266  mzpsubst  43267  pellexlem5  43348  pell14qrexpclnn0  43381  pellfundex  43401  qirropth  43423  monotuz  43456  congmul  43482  congsub  43485  mzpcong  43487  fzmaxdif  43496  jm2.15nn0  43518  idomsubgmo  43708  trclimalb2  44240  mnringmulrcld  44742  fourierdlem42  46661  fourierdlem48  46666  fourierdlem80  46698  prmdvdsfmtnof1lem1  48131  cycldlenngric  48488  gpgedgvtx1  48622  lidldomn1  48791  rngccatidALTV  48832  ringccatidALTV  48866  coe1sclmulval  48945  line2  49312  line2xlem  49313  line2x  49314  line2y  49315  itsclc0yqsol  49324  seposep  49485  iscnrm3rlem8  49506  iscnrm3llem2  49509