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  7125  f1oiso2  7293  fnsuppres  8131  frrlem4  8229  omeulem2  8508  uniinqs  8731  unxpdomlem3  9157  sup0  9376  fin23lem11  10230  reclem3pr  10962  dedekind  11297  addlid  11317  subaddmulsub  11601  dmdcan  11852  xaddass2  13170  xlt2add  13180  xadddi2  13217  expaddzlem  14030  expaddz  14031  expmulz  14033  expdiv  14038  expmordi  14092  pfxeq  14620  ccatopth2  14641  relexpaddnn  14976  o1add  15539  o1mul  15540  o1sub  15541  ntrivcvgmul  15827  prmexpb  16648  pcpremul  16773  pcdiv  16782  pcqmul  16783  pcqdiv  16787  4sqlem12  16886  f1ocpbllem  17446  ercpbl  17471  erlecpbl  17472  latjlej12  18379  latmlem12  18395  latj4  18413  gsumsgrpccat  18732  symgsssg  19364  symgfisg  19365  mndodcong  19439  cmn4  19698  ablsub4  19707  abladdsub4  19708  lsm4  19757  abvdom  20733  abvtrivd  20735  orngmul  20768  lspsnvs  21039  lspsneu  21048  lspfixed  21053  lspexch  21054  lsmcv  21066  lspsolvlem  21067  mvrf1  21911  coe1sclmulfv  22185  m1detdiag  22500  cnprest  23192  isreg2  23280  elptr  23476  hausflimlem  23882  trcfilu  24197  ssblps  24326  ssbl  24327  prdsxmslem2  24433  tgqioo  24704  metnrm  24767  bndth  24873  ncvspi  25072  cph2ass  25129  iscau3  25194  ovolunlem2  25415  dvres2  25829  dvfsumlem2  25949  dvfsumlem2OLD  25950  dvfsum2  25957  deg1tm  26040  plyadd  26138  plymul  26139  coeeu  26146  coemullem  26171  aalioulem4  26259  cxplea  26621  cxple2  26622  cxplt2  26623  cxple2a  26624  cxpcn3lem  26673  angcan  26728  ang180lem5  26739  divsqrtsumlem  26906  logexprlim  27152  dchrvmasumlema  27427  dchrisum0lema  27441  logdivsum  27460  log2sumbnd  27471  padicabv  27557  nolesgn2ores  27600  nogesgn1o  27601  nogesgn1ores  27602  nolt02o  27623  nogt01o  27624  nosupinfsep  27660  noetalem1  27669  noeta2  27713  scutbdaylt  27747  expsgt0  28347  tghilberti2  28601  brbtwn2  28868  axcontlem4  28930  axcontlem8  28934  clwlkl1loop  29746  chscllem4  31602  mdslmd4i  32295  nexple  32802  measxun2  34176  measun  34177  mbfmco2  34232  probun  34386  satfv1fvfmla1  35395  wsuclem  35798  cgrcomim  35962  cgrcoml  35969  cgrcomr  35970  cgrdegen  35977  btwnintr  35992  btwnexch3  35993  btwnouttr  35997  btwnexch  35998  btwndiff  36000  ifscgr  36017  lineid  36056  btwnconn1lem7  36066  btwnconn1lem8  36067  btwnconn1lem9  36068  btwnconn1lem12  36071  midofsegid  36077  brsegle2  36082  btwnoutside  36098  outsideoftr  36102  cnres2  37742  heibor  37800  lsmsat  38986  lkrlsp  39080  lkrlsp2  39081  lkrlsp3  39082  lshpkrlem6  39093  latm4  39211  omlspjN  39239  hlatj4  39352  4noncolr3  39432  4noncolr2  39433  4noncolr1  39434  3dimlem3a  39439  3dimlem4a  39442  3dimlem4  39443  3dimlem4OLDN  39444  1cvratex  39452  hlatexch4  39460  3atlem4  39465  atcvrlln2  39498  atcvrlln  39499  llnmlplnN  39518  lplnnlelln  39522  lvoli2  39560  lvolnlelln  39563  lvolnlelpln  39564  4atlem11b  39587  4atlem12b  39590  2lplnj  39599  dalemzeo  39612  dath2  39716  lncvrat  39761  cdlemb  39773  elpaddri  39781  padd4N  39819  llnmod2i2  39842  llnexchb2  39848  dalawlem1  39850  dalawlem2  39851  osumcllem6N  39940  pexmidlem3N  39951  pexmidlem4N  39952  lhp2lt  39980  lhp2at0  40011  lhp2atne  40013  lhp2at0ne  40015  lhpmod2i2  40017  lhpmod6i1  40018  lhpat  40022  lhpat3  40025  4atexlemex6  40053  ltrncoval  40124  ltrncnv  40125  ltrnnidn  40153  cdlemd7  40183  cdleme0b  40191  cdleme0c  40192  cdleme0fN  40197  cdleme0ex1N  40202  cdleme7d  40225  cdleme7e  40226  cdleme7ga  40227  cdleme7  40228  cdleme11a  40239  cdleme17c  40267  cdleme22gb  40273  cdlemeda  40277  cdleme20k  40298  cdleme21a  40304  cdleme21at  40307  cdleme21d  40309  cdleme22f2  40326  cdleme22g  40327  cdleme24  40331  cdleme28  40352  cdlemefrs29cpre1  40377  cdlemefr29exN  40381  cdlemefr32sn2aw  40383  cdleme32fva  40416  cdleme32fva1  40417  cdleme35a  40427  cdleme42c  40451  cdleme42e  40458  cdleme42f  40459  cdleme42g  40460  cdleme42h  40461  cdleme43bN  40469  cdleme46f2g2  40472  cdleme17d2  40474  cdleme4gfv  40486  cdlemeg46c  40492  cdlemeg46nlpq  40496  cdlemeg46gfre  40511  cdlemeg49lebilem  40518  cdleme50trn1  40528  cdleme50trn2  40530  cdleme50ltrn  40536  cdleme  40539  cdlemf1  40540  cdlemf  40542  trlord  40548  ltrniotavalbN  40563  cdlemg1cex  40567  cdlemg2dN  40569  cdlemg2ce  40571  cdlemg2fvlem  40573  cdlemg2idN  40575  cdlemg2kq  40581  cdlemg2l  40582  cdlemg7fvN  40603  cdlemg7aN  40604  cdlemg8a  40606  cdlemg11aq  40617  cdlemg12d  40625  cdlemg13a  40630  cdlemg13  40631  cdlemg14f  40632  cdlemg14g  40633  cdlemg17b  40641  cdlemg27a  40671  cdlemg31b0N  40673  cdlemg31a  40676  cdlemg31b  40677  cdlemg31c  40678  ltrnco  40698  trlcoabs2N  40701  trlcocnvat  40703  trlconid  40704  trlcolem  40705  cdlemg42  40708  cdlemg43  40709  cdlemg47a  40713  cdlemg46  40714  cdlemg47  40715  tendoeq1  40743  tendocoval  40745  tendoco2  40747  tendoplco2  40758  tendopltp  40759  cdlemh1  40794  cdlemh2  40795  cdlemi1  40797  cdlemi  40799  cdlemk1  40810  cdlemk2  40811  cdlemk3  40812  cdlemk4  40813  cdlemk8  40817  cdlemk9  40818  cdlemk9bN  40819  cdlemk31  40875  cdlemk28-3  40887  cdlemk19xlem  40921  cdlemk39u  40947  cdlemk19u  40949  cdlemk56w  40952  cdlemn7  41182  cdlemn8  41183  cdlemn9  41184  dihordlem6  41192  dihordlem7  41193  dihordlem7b  41194  dihord1  41197  dihord2a  41198  dihord11c  41203  dihord2pre  41204  dihord2pre2  41205  dihlsscpre  41213  dihord4  41237  dihord6b  41239  dihmeetlem2N  41278  dihglbcpreN  41279  dihmeetcN  41281  dihmeetbclemN  41283  dihmeetlem3N  41284  dihmeetlem9N  41294  dihmeetlem13N  41298  dihmeetlem20N  41305  mapdpglem24  41683  mapdpglem32  41684  baerlem3lem2  41689  baerlem5alem2  41690  baerlem5blem2  41691  mapdh9aOLDN  41769  hdmap14lem6  41852  nnadddir  42243  sn-addlid  42377  mzpmfp  42720  mzpsubst  42721  pellexlem5  42806  pell14qrexpclnn0  42839  pellfundex  42859  qirropth  42881  monotuz  42914  congmul  42940  congsub  42943  mzpcong  42945  fzmaxdif  42954  jm2.15nn0  42976  idomsubgmo  43166  trclimalb2  43699  mnringmulrcld  44201  fourierdlem42  46131  fourierdlem48  46136  fourierdlem80  46168  prmdvdsfmtnof1lem1  47569  cycldlenngric  47913  gpgedgvtx1  48047  lidldomn1  48216  rngccatidALTV  48257  ringccatidALTV  48291  coe1sclmulval  48371  line2  48738  line2xlem  48739  line2x  48740  line2y  48741  itsclc0yqsol  48750  seposep  48911  iscnrm3rlem8  48932  iscnrm3llem2  48935