Theorem simp2r 1200

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 485	. 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜒)
2	1	3ad2ant2 1134	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1087

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 397  df-3an 1089

This theorem is referenced by:  simp12r  1287  simp22r  1293  simp32r  1299  fsnunf  7182  f1oiso2  7348  fnsuppres  8175  frrlem4  8273  omeulem2  8582  uniinqs  8790  unxpdomlem3  9251  sup0  9460  fin23lem11  10311  reclem3pr  11043  dedekind  11376  addlid  11396  subaddmulsub  11676  dmdcan  11923  xaddass2  13228  xlt2add  13238  xadddi2  13275  expaddzlem  14070  expaddz  14071  expmulz  14073  expdiv  14078  expmordi  14131  pfxeq  14645  ccatopth2  14666  relexpaddnn  14997  o1add  15557  o1mul  15558  o1sub  15559  ntrivcvgmul  15847  prmexpb  16656  pcpremul  16775  pcdiv  16784  pcqmul  16785  pcqdiv  16789  4sqlem12  16888  f1ocpbllem  17469  ercpbl  17494  erlecpbl  17495  latjlej12  18407  latmlem12  18423  latj4  18441  gsumsgrpccat  18720  symgsssg  19334  symgfisg  19335  mndodcong  19409  cmn4  19668  ablsub4  19677  abladdsub4  19678  lsm4  19727  abvdom  20445  abvtrivd  20447  lspsnvs  20726  lspsneu  20735  lspfixed  20740  lspexch  20741  lsmcv  20753  lspsolvlem  20754  mvrf1  21544  coe1sclmulfv  21804  m1detdiag  22098  cnprest  22792  isreg2  22880  elptr  23076  hausflimlem  23482  trcfilu  23798  ssblps  23927  ssbl  23928  prdsxmslem2  24037  tgqioo  24315  metnrm  24377  bndth  24473  ncvspi  24672  cph2ass  24729  iscau3  24794  ovolunlem2  25014  dvres2  25428  dvfsumlem2  25543  dvfsum2  25550  deg1tm  25635  plyadd  25730  plymul  25731  coeeu  25738  coemullem  25763  aalioulem4  25847  cxplea  26203  cxple2  26204  cxplt2  26205  cxple2a  26206  cxpcn3lem  26252  angcan  26304  ang180lem5  26315  divsqrtsumlem  26481  logexprlim  26725  dchrvmasumlema  27000  dchrisum0lema  27014  logdivsum  27033  log2sumbnd  27044  padicabv  27130  nolesgn2ores  27172  nogesgn1o  27173  nogesgn1ores  27174  nolt02o  27195  nogt01o  27196  nosupinfsep  27232  noetalem1  27241  noeta2  27283  scutbdaylt  27316  tghilberti2  27886  brbtwn2  28160  axcontlem4  28222  axcontlem8  28226  clwlkl1loop  29037  chscllem4  30888  mdslmd4i  31581  orngmul  32416  nexple  33002  measxun2  33203  measun  33204  mbfmco2  33259  probun  33413  satfv1fvfmla1  34409  wsuclem  34792  cgrcomim  34956  cgrcoml  34963  cgrcomr  34964  cgrdegen  34971  btwnintr  34986  btwnexch3  34987  btwnouttr  34991  btwnexch  34992  btwndiff  34994  ifscgr  35011  lineid  35050  btwnconn1lem7  35060  btwnconn1lem8  35061  btwnconn1lem9  35062  btwnconn1lem12  35065  midofsegid  35071  brsegle2  35076  btwnoutside  35092  outsideoftr  35096  gg-dvfsumlem2  35178  cnres2  36626  heibor  36684  lsmsat  37873  lkrlsp  37967  lkrlsp2  37968  lkrlsp3  37969  lshpkrlem6  37980  latm4  38098  omlspjN  38126  hlatj4  38239  4noncolr3  38319  4noncolr2  38320  4noncolr1  38321  3dimlem3a  38326  3dimlem4a  38329  3dimlem4  38330  3dimlem4OLDN  38331  1cvratex  38339  hlatexch4  38347  3atlem4  38352  atcvrlln2  38385  atcvrlln  38386  llnmlplnN  38405  lplnnlelln  38409  lvoli2  38447  lvolnlelln  38450  lvolnlelpln  38451  4atlem11b  38474  4atlem12b  38477  2lplnj  38486  dalemzeo  38499  dath2  38603  lncvrat  38648  cdlemb  38660  elpaddri  38668  padd4N  38706  llnmod2i2  38729  llnexchb2  38735  dalawlem1  38737  dalawlem2  38738  osumcllem6N  38827  pexmidlem3N  38838  pexmidlem4N  38839  lhp2lt  38867  lhp2at0  38898  lhp2atne  38900  lhp2at0ne  38902  lhpmod2i2  38904  lhpmod6i1  38905  lhpat  38909  lhpat3  38912  4atexlemex6  38940  ltrncoval  39011  ltrncnv  39012  ltrnnidn  39040  cdlemd7  39070  cdleme0b  39078  cdleme0c  39079  cdleme0fN  39084  cdleme0ex1N  39089  cdleme7d  39112  cdleme7e  39113  cdleme7ga  39114  cdleme7  39115  cdleme11a  39126  cdleme17c  39154  cdleme22gb  39160  cdlemeda  39164  cdleme20k  39185  cdleme21a  39191  cdleme21at  39194  cdleme21d  39196  cdleme22f2  39213  cdleme22g  39214  cdleme24  39218  cdleme28  39239  cdlemefrs29cpre1  39264  cdlemefr29exN  39268  cdlemefr32sn2aw  39270  cdleme32fva  39303  cdleme32fva1  39304  cdleme35a  39314  cdleme42c  39338  cdleme42e  39345  cdleme42f  39346  cdleme42g  39347  cdleme42h  39348  cdleme43bN  39356  cdleme46f2g2  39359  cdleme17d2  39361  cdleme4gfv  39373  cdlemeg46c  39379  cdlemeg46nlpq  39383  cdlemeg46gfre  39398  cdlemeg49lebilem  39405  cdleme50trn1  39415  cdleme50trn2  39417  cdleme50ltrn  39423  cdleme  39426  cdlemf1  39427  cdlemf  39429  trlord  39435  ltrniotavalbN  39450  cdlemg1cex  39454  cdlemg2dN  39456  cdlemg2ce  39458  cdlemg2fvlem  39460  cdlemg2idN  39462  cdlemg2kq  39468  cdlemg2l  39469  cdlemg7fvN  39490  cdlemg7aN  39491  cdlemg8a  39493  cdlemg11aq  39504  cdlemg12d  39512  cdlemg13a  39517  cdlemg13  39518  cdlemg14f  39519  cdlemg14g  39520  cdlemg17b  39528  cdlemg27a  39558  cdlemg31b0N  39560  cdlemg31a  39563  cdlemg31b  39564  cdlemg31c  39565  ltrnco  39585  trlcoabs2N  39588  trlcocnvat  39590  trlconid  39591  trlcolem  39592  cdlemg42  39595  cdlemg43  39596  cdlemg47a  39600  cdlemg46  39601  cdlemg47  39602  tendoeq1  39630  tendocoval  39632  tendoco2  39634  tendoplco2  39645  tendopltp  39646  cdlemh1  39681  cdlemh2  39682  cdlemi1  39684  cdlemi  39686  cdlemk1  39697  cdlemk2  39698  cdlemk3  39699  cdlemk4  39700  cdlemk8  39704  cdlemk9  39705  cdlemk9bN  39706  cdlemk31  39762  cdlemk28-3  39774  cdlemk19xlem  39808  cdlemk39u  39834  cdlemk19u  39836  cdlemk56w  39839  cdlemn7  40069  cdlemn8  40070  cdlemn9  40071  dihordlem6  40079  dihordlem7  40080  dihordlem7b  40081  dihord1  40084  dihord2a  40085  dihord11c  40090  dihord2pre  40091  dihord2pre2  40092  dihlsscpre  40100  dihord4  40124  dihord6b  40126  dihmeetlem2N  40165  dihglbcpreN  40166  dihmeetcN  40168  dihmeetbclemN  40170  dihmeetlem3N  40171  dihmeetlem9N  40181  dihmeetlem13N  40185  dihmeetlem20N  40192  mapdpglem24  40570  mapdpglem32  40571  baerlem3lem2  40576  baerlem5alem2  40577  baerlem5blem2  40578  mapdh9aOLDN  40656  hdmap14lem6  40739  nnadddir  41186  sn-addlid  41278  mzpmfp  41475  mzpsubst  41476  pellexlem5  41561  pell14qrexpclnn0  41594  pellfundex  41614  qirropth  41636  monotuz  41670  congmul  41696  congsub  41699  mzpcong  41701  fzmaxdif  41710  jm2.15nn0  41732  idomsubgmo  41930  trclimalb2  42467  mnringmulrcld  42977  fourierdlem42  44855  fourierdlem48  44860  fourierdlem80  44892  prmdvdsfmtnof1lem1  46242  lidldomn1  46813  rngccatidALTV  46877  ringccatidALTV  46940  coe1sclmulval  47056  line2  47428  line2xlem  47429  line2x  47430  line2y  47431  itsclc0yqsol  47440  seposep  47548  iscnrm3rlem8  47570  iscnrm3llem2  47573