Theorem simp2r 1201

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 484	. 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜒)
2	1	3ad2ant2 1134	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:  simp12r  1288  simp22r  1294  simp32r  1300  fsnunf  7159  f1oiso2  7327  fnsuppres  8170  frrlem4  8268  omeulem2  8547  uniinqs  8770  unxpdomlem3  9199  sup0  9418  fin23lem11  10270  reclem3pr  11002  dedekind  11337  addlid  11357  subaddmulsub  11641  dmdcan  11892  xaddass2  13210  xlt2add  13220  xadddi2  13257  expaddzlem  14070  expaddz  14071  expmulz  14073  expdiv  14078  expmordi  14132  pfxeq  14661  ccatopth2  14682  relexpaddnn  15017  o1add  15580  o1mul  15581  o1sub  15582  ntrivcvgmul  15868  prmexpb  16689  pcpremul  16814  pcdiv  16823  pcqmul  16824  pcqdiv  16828  4sqlem12  16927  f1ocpbllem  17487  ercpbl  17512  erlecpbl  17513  latjlej12  18414  latmlem12  18430  latj4  18448  gsumsgrpccat  18767  symgsssg  19397  symgfisg  19398  mndodcong  19472  cmn4  19731  ablsub4  19740  abladdsub4  19741  lsm4  19790  abvdom  20739  abvtrivd  20741  lspsnvs  21024  lspsneu  21033  lspfixed  21038  lspexch  21039  lsmcv  21051  lspsolvlem  21052  mvrf1  21895  coe1sclmulfv  22169  m1detdiag  22484  cnprest  23176  isreg2  23264  elptr  23460  hausflimlem  23866  trcfilu  24181  ssblps  24310  ssbl  24311  prdsxmslem2  24417  tgqioo  24688  metnrm  24751  bndth  24857  ncvspi  25056  cph2ass  25113  iscau3  25178  ovolunlem2  25399  dvres2  25813  dvfsumlem2  25933  dvfsumlem2OLD  25934  dvfsum2  25941  deg1tm  26024  plyadd  26122  plymul  26123  coeeu  26130  coemullem  26155  aalioulem4  26243  cxplea  26605  cxple2  26606  cxplt2  26607  cxple2a  26608  cxpcn3lem  26657  angcan  26712  ang180lem5  26723  divsqrtsumlem  26890  logexprlim  27136  dchrvmasumlema  27411  dchrisum0lema  27425  logdivsum  27444  log2sumbnd  27455  padicabv  27541  nolesgn2ores  27584  nogesgn1o  27585  nogesgn1ores  27586  nolt02o  27607  nogt01o  27608  nosupinfsep  27644  noetalem1  27653  noeta2  27696  scutbdaylt  27730  expsgt0  28322  tghilberti2  28565  brbtwn2  28832  axcontlem4  28894  axcontlem8  28898  clwlkl1loop  29713  chscllem4  31569  mdslmd4i  32262  nexple  32769  orngmul  33281  measxun2  34200  measun  34201  mbfmco2  34256  probun  34410  satfv1fvfmla1  35410  wsuclem  35813  cgrcomim  35977  cgrcoml  35984  cgrcomr  35985  cgrdegen  35992  btwnintr  36007  btwnexch3  36008  btwnouttr  36012  btwnexch  36013  btwndiff  36015  ifscgr  36032  lineid  36071  btwnconn1lem7  36081  btwnconn1lem8  36082  btwnconn1lem9  36083  btwnconn1lem12  36086  midofsegid  36092  brsegle2  36097  btwnoutside  36113  outsideoftr  36117  cnres2  37757  heibor  37815  lsmsat  39001  lkrlsp  39095  lkrlsp2  39096  lkrlsp3  39097  lshpkrlem6  39108  latm4  39226  omlspjN  39254  hlatj4  39367  4noncolr3  39447  4noncolr2  39448  4noncolr1  39449  3dimlem3a  39454  3dimlem4a  39457  3dimlem4  39458  3dimlem4OLDN  39459  1cvratex  39467  hlatexch4  39475  3atlem4  39480  atcvrlln2  39513  atcvrlln  39514  llnmlplnN  39533  lplnnlelln  39537  lvoli2  39575  lvolnlelln  39578  lvolnlelpln  39579  4atlem11b  39602  4atlem12b  39605  2lplnj  39614  dalemzeo  39627  dath2  39731  lncvrat  39776  cdlemb  39788  elpaddri  39796  padd4N  39834  llnmod2i2  39857  llnexchb2  39863  dalawlem1  39865  dalawlem2  39866  osumcllem6N  39955  pexmidlem3N  39966  pexmidlem4N  39967  lhp2lt  39995  lhp2at0  40026  lhp2atne  40028  lhp2at0ne  40030  lhpmod2i2  40032  lhpmod6i1  40033  lhpat  40037  lhpat3  40040  4atexlemex6  40068  ltrncoval  40139  ltrncnv  40140  ltrnnidn  40168  cdlemd7  40198  cdleme0b  40206  cdleme0c  40207  cdleme0fN  40212  cdleme0ex1N  40217  cdleme7d  40240  cdleme7e  40241  cdleme7ga  40242  cdleme7  40243  cdleme11a  40254  cdleme17c  40282  cdleme22gb  40288  cdlemeda  40292  cdleme20k  40313  cdleme21a  40319  cdleme21at  40322  cdleme21d  40324  cdleme22f2  40341  cdleme22g  40342  cdleme24  40346  cdleme28  40367  cdlemefrs29cpre1  40392  cdlemefr29exN  40396  cdlemefr32sn2aw  40398  cdleme32fva  40431  cdleme32fva1  40432  cdleme35a  40442  cdleme42c  40466  cdleme42e  40473  cdleme42f  40474  cdleme42g  40475  cdleme42h  40476  cdleme43bN  40484  cdleme46f2g2  40487  cdleme17d2  40489  cdleme4gfv  40501  cdlemeg46c  40507  cdlemeg46nlpq  40511  cdlemeg46gfre  40526  cdlemeg49lebilem  40533  cdleme50trn1  40543  cdleme50trn2  40545  cdleme50ltrn  40551  cdleme  40554  cdlemf1  40555  cdlemf  40557  trlord  40563  ltrniotavalbN  40578  cdlemg1cex  40582  cdlemg2dN  40584  cdlemg2ce  40586  cdlemg2fvlem  40588  cdlemg2idN  40590  cdlemg2kq  40596  cdlemg2l  40597  cdlemg7fvN  40618  cdlemg7aN  40619  cdlemg8a  40621  cdlemg11aq  40632  cdlemg12d  40640  cdlemg13a  40645  cdlemg13  40646  cdlemg14f  40647  cdlemg14g  40648  cdlemg17b  40656  cdlemg27a  40686  cdlemg31b0N  40688  cdlemg31a  40691  cdlemg31b  40692  cdlemg31c  40693  ltrnco  40713  trlcoabs2N  40716  trlcocnvat  40718  trlconid  40719  trlcolem  40720  cdlemg42  40723  cdlemg43  40724  cdlemg47a  40728  cdlemg46  40729  cdlemg47  40730  tendoeq1  40758  tendocoval  40760  tendoco2  40762  tendoplco2  40773  tendopltp  40774  cdlemh1  40809  cdlemh2  40810  cdlemi1  40812  cdlemi  40814  cdlemk1  40825  cdlemk2  40826  cdlemk3  40827  cdlemk4  40828  cdlemk8  40832  cdlemk9  40833  cdlemk9bN  40834  cdlemk31  40890  cdlemk28-3  40902  cdlemk19xlem  40936  cdlemk39u  40962  cdlemk19u  40964  cdlemk56w  40967  cdlemn7  41197  cdlemn8  41198  cdlemn9  41199  dihordlem6  41207  dihordlem7  41208  dihordlem7b  41209  dihord1  41212  dihord2a  41213  dihord11c  41218  dihord2pre  41219  dihord2pre2  41220  dihlsscpre  41228  dihord4  41252  dihord6b  41254  dihmeetlem2N  41293  dihglbcpreN  41294  dihmeetcN  41296  dihmeetbclemN  41298  dihmeetlem3N  41299  dihmeetlem9N  41309  dihmeetlem13N  41313  dihmeetlem20N  41320  mapdpglem24  41698  mapdpglem32  41699  baerlem3lem2  41704  baerlem5alem2  41705  baerlem5blem2  41706  mapdh9aOLDN  41784  hdmap14lem6  41867  nnadddir  42258  sn-addlid  42392  mzpmfp  42735  mzpsubst  42736  pellexlem5  42821  pell14qrexpclnn0  42854  pellfundex  42874  qirropth  42896  monotuz  42930  congmul  42956  congsub  42959  mzpcong  42961  fzmaxdif  42970  jm2.15nn0  42992  idomsubgmo  43182  trclimalb2  43715  mnringmulrcld  44217  fourierdlem42  46147  fourierdlem48  46152  fourierdlem80  46184  prmdvdsfmtnof1lem1  47585  cycldlenngric  47928  gpgedgvtx1  48053  lidldomn1  48219  rngccatidALTV  48260  ringccatidALTV  48294  coe1sclmulval  48374  line2  48741  line2xlem  48742  line2x  48743  line2y  48744  itsclc0yqsol  48753  seposep  48914  iscnrm3rlem8  48935  iscnrm3llem2  48938