Theorem simp2r 1196

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 1130	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1083

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 1085

This theorem is referenced by:  simp12r  1283  simp22r  1289  simp32r  1295  fsnunf  6946  f1oiso2  7104  fnsuppres  7856  omeulem2  8208  uniinqs  8376  unxpdomlem3  8723  sup0  8929  fin23lem11  9738  reclem3pr  10470  dedekind  10802  addid2  10822  subaddmulsub  11102  dmdcan  11349  xaddass2  12642  xlt2add  12652  xadddi2  12689  expaddzlem  13471  expaddz  13472  expmulz  13474  expdiv  13479  expmordi  13530  pfxeq  14057  ccatopth2  14078  relexpaddnn  14409  o1add  14969  o1mul  14970  o1sub  14971  ntrivcvgmul  15257  prmexpb  16061  pcpremul  16179  pcdiv  16188  pcqmul  16189  pcqdiv  16193  4sqlem12  16291  f1ocpbllem  16796  ercpbl  16821  erlecpbl  16822  latjlej12  17676  latmlem12  17692  latj4  17710  gsumsgrpccat  18003  symgsssg  18594  symgfisg  18595  mndodcong  18669  cmn4  18925  ablsub4  18932  abladdsub4  18933  lsm4  18979  abvdom  19608  abvtrivd  19610  lspsnvs  19885  lspsneu  19894  lspfixed  19899  lspexch  19900  lsmcv  19912  lspsolvlem  19913  mvrf1  20204  coe1sclmulfv  20450  m1detdiag  21205  cnprest  21896  isreg2  21984  elptr  22180  hausflimlem  22586  trcfilu  22902  ssblps  23031  ssbl  23032  prdsxmslem2  23138  tgqioo  23407  metnrm  23469  bndth  23561  ncvspi  23759  cph2ass  23816  iscau3  23880  ovolunlem2  24098  dvres2  24509  dvfsumlem2  24623  dvfsum2  24630  deg1tm  24711  plyadd  24806  plymul  24807  coeeu  24814  coemullem  24839  aalioulem4  24923  cxplea  25278  cxple2  25279  cxplt2  25280  cxple2a  25281  cxpcn3lem  25327  angcan  25379  ang180lem5  25390  divsqrtsumlem  25556  logexprlim  25800  dchrvmasumlema  26075  dchrisum0lema  26089  logdivsum  26108  log2sumbnd  26119  padicabv  26205  tghilberti2  26423  brbtwn2  26690  axcontlem4  26752  axcontlem8  26756  clwlkl1loop  27563  chscllem4  29416  mdslmd4i  30109  orngmul  30876  nexple  31268  measxun2  31469  measun  31470  mbfmco2  31523  probun  31677  satfv1fvfmla1  32670  wsuclem  33112  frrlem4  33126  nolesgn2ores  33179  nolt02o  33199  noetalem5  33221  scutbdaylt  33276  cgrcomim  33450  cgrcoml  33457  cgrcomr  33458  cgrdegen  33465  btwnintr  33480  btwnexch3  33481  btwnouttr  33485  btwnexch  33486  btwndiff  33488  ifscgr  33505  lineid  33544  btwnconn1lem7  33554  btwnconn1lem8  33555  btwnconn1lem9  33556  btwnconn1lem12  33559  midofsegid  33565  brsegle2  33570  btwnoutside  33586  outsideoftr  33590  cnres2  35040  heibor  35098  lsmsat  36143  lkrlsp  36237  lkrlsp2  36238  lkrlsp3  36239  lshpkrlem6  36250  latm4  36368  omlspjN  36396  hlatj4  36509  4noncolr3  36588  4noncolr2  36589  4noncolr1  36590  3dimlem3a  36595  3dimlem4a  36598  3dimlem4  36599  3dimlem4OLDN  36600  1cvratex  36608  hlatexch4  36616  3atlem4  36621  atcvrlln2  36654  atcvrlln  36655  llnmlplnN  36674  lplnnlelln  36678  lvoli2  36716  lvolnlelln  36719  lvolnlelpln  36720  4atlem11b  36743  4atlem12b  36746  2lplnj  36755  dalemzeo  36768  dath2  36872  lncvrat  36917  cdlemb  36929  elpaddri  36937  padd4N  36975  llnmod2i2  36998  llnexchb2  37004  dalawlem1  37006  dalawlem2  37007  osumcllem6N  37096  pexmidlem3N  37107  pexmidlem4N  37108  lhp2lt  37136  lhp2at0  37167  lhp2atne  37169  lhp2at0ne  37171  lhpmod2i2  37173  lhpmod6i1  37174  lhpat  37178  lhpat3  37181  4atexlemex6  37209  ltrncoval  37280  ltrncnv  37281  ltrnnidn  37309  cdlemd7  37339  cdleme0b  37347  cdleme0c  37348  cdleme0fN  37353  cdleme0ex1N  37358  cdleme7d  37381  cdleme7e  37382  cdleme7ga  37383  cdleme7  37384  cdleme11a  37395  cdleme17c  37423  cdleme22gb  37429  cdlemeda  37433  cdleme20k  37454  cdleme21a  37460  cdleme21at  37463  cdleme21d  37465  cdleme22f2  37482  cdleme22g  37483  cdleme24  37487  cdleme28  37508  cdlemefrs29cpre1  37533  cdlemefr29exN  37537  cdlemefr32sn2aw  37539  cdleme32fva  37572  cdleme32fva1  37573  cdleme35a  37583  cdleme42c  37607  cdleme42e  37614  cdleme42f  37615  cdleme42g  37616  cdleme42h  37617  cdleme43bN  37625  cdleme46f2g2  37628  cdleme17d2  37630  cdleme4gfv  37642  cdlemeg46c  37648  cdlemeg46nlpq  37652  cdlemeg46gfre  37667  cdlemeg49lebilem  37674  cdleme50trn1  37684  cdleme50trn2  37686  cdleme50ltrn  37692  cdleme  37695  cdlemf1  37696  cdlemf  37698  trlord  37704  ltrniotavalbN  37719  cdlemg1cex  37723  cdlemg2dN  37725  cdlemg2ce  37727  cdlemg2fvlem  37729  cdlemg2idN  37731  cdlemg2kq  37737  cdlemg2l  37738  cdlemg7fvN  37759  cdlemg7aN  37760  cdlemg8a  37762  cdlemg11aq  37773  cdlemg12d  37781  cdlemg13a  37786  cdlemg13  37787  cdlemg14f  37788  cdlemg14g  37789  cdlemg17b  37797  cdlemg27a  37827  cdlemg31b0N  37829  cdlemg31a  37832  cdlemg31b  37833  cdlemg31c  37834  ltrnco  37854  trlcoabs2N  37857  trlcocnvat  37859  trlconid  37860  trlcolem  37861  cdlemg42  37864  cdlemg43  37865  cdlemg47a  37869  cdlemg46  37870  cdlemg47  37871  tendoeq1  37899  tendocoval  37901  tendoco2  37903  tendoplco2  37914  tendopltp  37915  cdlemh1  37950  cdlemh2  37951  cdlemi1  37953  cdlemi  37955  cdlemk1  37966  cdlemk2  37967  cdlemk3  37968  cdlemk4  37969  cdlemk8  37973  cdlemk9  37974  cdlemk9bN  37975  cdlemk31  38031  cdlemk28-3  38043  cdlemk19xlem  38077  cdlemk39u  38103  cdlemk19u  38105  cdlemk56w  38108  cdlemn7  38338  cdlemn8  38339  cdlemn9  38340  dihordlem6  38348  dihordlem7  38349  dihordlem7b  38350  dihord1  38353  dihord2a  38354  dihord11c  38359  dihord2pre  38360  dihord2pre2  38361  dihlsscpre  38369  dihord4  38393  dihord6b  38395  dihmeetlem2N  38434  dihglbcpreN  38435  dihmeetcN  38437  dihmeetbclemN  38439  dihmeetlem3N  38440  dihmeetlem9N  38450  dihmeetlem13N  38454  dihmeetlem20N  38461  mapdpglem24  38839  mapdpglem32  38840  baerlem3lem2  38845  baerlem5alem2  38846  baerlem5blem2  38847  mapdh9aOLDN  38925  hdmap14lem6  39008  nnadddir  39161  sn-addid2  39232  mzpmfp  39342  mzpsubst  39343  pellexlem5  39428  pell14qrexpclnn0  39461  pellfundex  39481  qirropth  39503  monotuz  39536  congmul  39562  congsub  39565  mzpcong  39567  fzmaxdif  39576  jm2.15nn0  39598  idomsubgmo  39796  trclimalb2  40069  fourierdlem42  42433  fourierdlem48  42438  fourierdlem80  42470  prmdvdsfmtnof1lem1  43745  lidldomn1  44191  rngccatidALTV  44259  ringccatidALTV  44322  coe1sclmulval  44438  line2  44738  line2xlem  44739  line2x  44740  line2y  44741  itsclc0yqsol  44750