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 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  1287  simp22r  1293  simp32r  1299  fsnunf  7187  f1oiso2  7354  fnsuppres  8198  frrlem4  8296  omeulem2  8603  uniinqs  8819  unxpdomlem3  9270  sup0  9488  fin23lem11  10339  reclem3pr  11071  dedekind  11406  addlid  11426  subaddmulsub  11708  dmdcan  11959  xaddass2  13274  xlt2add  13284  xadddi2  13321  expaddzlem  14128  expaddz  14129  expmulz  14131  expdiv  14136  expmordi  14189  pfxeq  14716  ccatopth2  14737  relexpaddnn  15072  o1add  15632  o1mul  15633  o1sub  15634  ntrivcvgmul  15920  prmexpb  16738  pcpremul  16863  pcdiv  16872  pcqmul  16873  pcqdiv  16877  4sqlem12  16976  f1ocpbllem  17540  ercpbl  17565  erlecpbl  17566  latjlej12  18469  latmlem12  18485  latj4  18503  gsumsgrpccat  18822  symgsssg  19453  symgfisg  19454  mndodcong  19528  cmn4  19787  ablsub4  19796  abladdsub4  19797  lsm4  19846  abvdom  20799  abvtrivd  20801  lspsnvs  21084  lspsneu  21093  lspfixed  21098  lspexch  21099  lsmcv  21111  lspsolvlem  21112  mvrf1  21960  coe1sclmulfv  22234  m1detdiag  22551  cnprest  23243  isreg2  23331  elptr  23527  hausflimlem  23933  trcfilu  24248  ssblps  24377  ssbl  24378  prdsxmslem2  24486  tgqioo  24757  metnrm  24820  bndth  24926  ncvspi  25126  cph2ass  25183  iscau3  25248  ovolunlem2  25469  dvres2  25883  dvfsumlem2  26003  dvfsumlem2OLD  26004  dvfsum2  26011  deg1tm  26094  plyadd  26192  plymul  26193  coeeu  26200  coemullem  26225  aalioulem4  26313  cxplea  26674  cxple2  26675  cxplt2  26676  cxple2a  26677  cxpcn3lem  26726  angcan  26781  ang180lem5  26792  divsqrtsumlem  26959  logexprlim  27205  dchrvmasumlema  27480  dchrisum0lema  27494  logdivsum  27513  log2sumbnd  27524  padicabv  27610  nolesgn2ores  27653  nogesgn1o  27654  nogesgn1ores  27655  nolt02o  27676  nogt01o  27677  nosupinfsep  27713  noetalem1  27722  noeta2  27765  scutbdaylt  27799  expsgt0  28351  tghilberti2  28582  brbtwn2  28850  axcontlem4  28912  axcontlem8  28916  clwlkl1loop  29731  chscllem4  31587  mdslmd4i  32280  nexple  32773  orngmul  33273  measxun2  34170  measun  34171  mbfmco2  34226  probun  34380  satfv1fvfmla1  35387  wsuclem  35785  cgrcomim  35949  cgrcoml  35956  cgrcomr  35957  cgrdegen  35964  btwnintr  35979  btwnexch3  35980  btwnouttr  35984  btwnexch  35985  btwndiff  35987  ifscgr  36004  lineid  36043  btwnconn1lem7  36053  btwnconn1lem8  36054  btwnconn1lem9  36055  btwnconn1lem12  36058  midofsegid  36064  brsegle2  36069  btwnoutside  36085  outsideoftr  36089  cnres2  37729  heibor  37787  lsmsat  38968  lkrlsp  39062  lkrlsp2  39063  lkrlsp3  39064  lshpkrlem6  39075  latm4  39193  omlspjN  39221  hlatj4  39334  4noncolr3  39414  4noncolr2  39415  4noncolr1  39416  3dimlem3a  39421  3dimlem4a  39424  3dimlem4  39425  3dimlem4OLDN  39426  1cvratex  39434  hlatexch4  39442  3atlem4  39447  atcvrlln2  39480  atcvrlln  39481  llnmlplnN  39500  lplnnlelln  39504  lvoli2  39542  lvolnlelln  39545  lvolnlelpln  39546  4atlem11b  39569  4atlem12b  39572  2lplnj  39581  dalemzeo  39594  dath2  39698  lncvrat  39743  cdlemb  39755  elpaddri  39763  padd4N  39801  llnmod2i2  39824  llnexchb2  39830  dalawlem1  39832  dalawlem2  39833  osumcllem6N  39922  pexmidlem3N  39933  pexmidlem4N  39934  lhp2lt  39962  lhp2at0  39993  lhp2atne  39995  lhp2at0ne  39997  lhpmod2i2  39999  lhpmod6i1  40000  lhpat  40004  lhpat3  40007  4atexlemex6  40035  ltrncoval  40106  ltrncnv  40107  ltrnnidn  40135  cdlemd7  40165  cdleme0b  40173  cdleme0c  40174  cdleme0fN  40179  cdleme0ex1N  40184  cdleme7d  40207  cdleme7e  40208  cdleme7ga  40209  cdleme7  40210  cdleme11a  40221  cdleme17c  40249  cdleme22gb  40255  cdlemeda  40259  cdleme20k  40280  cdleme21a  40286  cdleme21at  40289  cdleme21d  40291  cdleme22f2  40308  cdleme22g  40309  cdleme24  40313  cdleme28  40334  cdlemefrs29cpre1  40359  cdlemefr29exN  40363  cdlemefr32sn2aw  40365  cdleme32fva  40398  cdleme32fva1  40399  cdleme35a  40409  cdleme42c  40433  cdleme42e  40440  cdleme42f  40441  cdleme42g  40442  cdleme42h  40443  cdleme43bN  40451  cdleme46f2g2  40454  cdleme17d2  40456  cdleme4gfv  40468  cdlemeg46c  40474  cdlemeg46nlpq  40478  cdlemeg46gfre  40493  cdlemeg49lebilem  40500  cdleme50trn1  40510  cdleme50trn2  40512  cdleme50ltrn  40518  cdleme  40521  cdlemf1  40522  cdlemf  40524  trlord  40530  ltrniotavalbN  40545  cdlemg1cex  40549  cdlemg2dN  40551  cdlemg2ce  40553  cdlemg2fvlem  40555  cdlemg2idN  40557  cdlemg2kq  40563  cdlemg2l  40564  cdlemg7fvN  40585  cdlemg7aN  40586  cdlemg8a  40588  cdlemg11aq  40599  cdlemg12d  40607  cdlemg13a  40612  cdlemg13  40613  cdlemg14f  40614  cdlemg14g  40615  cdlemg17b  40623  cdlemg27a  40653  cdlemg31b0N  40655  cdlemg31a  40658  cdlemg31b  40659  cdlemg31c  40660  ltrnco  40680  trlcoabs2N  40683  trlcocnvat  40685  trlconid  40686  trlcolem  40687  cdlemg42  40690  cdlemg43  40691  cdlemg47a  40695  cdlemg46  40696  cdlemg47  40697  tendoeq1  40725  tendocoval  40727  tendoco2  40729  tendoplco2  40740  tendopltp  40741  cdlemh1  40776  cdlemh2  40777  cdlemi1  40779  cdlemi  40781  cdlemk1  40792  cdlemk2  40793  cdlemk3  40794  cdlemk4  40795  cdlemk8  40799  cdlemk9  40800  cdlemk9bN  40801  cdlemk31  40857  cdlemk28-3  40869  cdlemk19xlem  40903  cdlemk39u  40929  cdlemk19u  40931  cdlemk56w  40934  cdlemn7  41164  cdlemn8  41165  cdlemn9  41166  dihordlem6  41174  dihordlem7  41175  dihordlem7b  41176  dihord1  41179  dihord2a  41180  dihord11c  41185  dihord2pre  41186  dihord2pre2  41187  dihlsscpre  41195  dihord4  41219  dihord6b  41221  dihmeetlem2N  41260  dihglbcpreN  41261  dihmeetcN  41263  dihmeetbclemN  41265  dihmeetlem3N  41266  dihmeetlem9N  41276  dihmeetlem13N  41280  dihmeetlem20N  41287  mapdpglem24  41665  mapdpglem32  41666  baerlem3lem2  41671  baerlem5alem2  41672  baerlem5blem2  41673  mapdh9aOLDN  41751  hdmap14lem6  41834  nnadddir  42268  sn-addlid  42397  mzpmfp  42721  mzpsubst  42722  pellexlem5  42807  pell14qrexpclnn0  42840  pellfundex  42860  qirropth  42882  monotuz  42916  congmul  42942  congsub  42945  mzpcong  42947  fzmaxdif  42956  jm2.15nn0  42978  idomsubgmo  43168  trclimalb2  43701  mnringmulrcld  44204  fourierdlem42  46121  fourierdlem48  46126  fourierdlem80  46158  prmdvdsfmtnof1lem1  47529  gpgedgvtx1  47978  lidldomn1  48105  rngccatidALTV  48146  ringccatidALTV  48180  coe1sclmulval  48260  line2  48631  line2xlem  48632  line2x  48633  line2y  48634  itsclc0yqsol  48643  seposep  48783  iscnrm3rlem8  48804  iscnrm3llem2  48807