Theorem simp2r 1197

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1084

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 396  df-3an 1086

This theorem is referenced by:  simp12r  1284  simp22r  1290  simp32r  1296  fsnunf  7178  f1oiso2  7344  fnsuppres  8173  frrlem4  8272  omeulem2  8581  uniinqs  8790  unxpdomlem3  9251  sup0  9460  fin23lem11  10311  reclem3pr  11043  dedekind  11378  addlid  11398  subaddmulsub  11678  dmdcan  11925  xaddass2  13232  xlt2add  13242  xadddi2  13279  expaddzlem  14074  expaddz  14075  expmulz  14077  expdiv  14082  expmordi  14135  pfxeq  14650  ccatopth2  14671  relexpaddnn  15002  o1add  15562  o1mul  15563  o1sub  15564  ntrivcvgmul  15852  prmexpb  16662  pcpremul  16783  pcdiv  16792  pcqmul  16793  pcqdiv  16797  4sqlem12  16896  f1ocpbllem  17477  ercpbl  17502  erlecpbl  17503  latjlej12  18418  latmlem12  18434  latj4  18452  gsumsgrpccat  18763  symgsssg  19385  symgfisg  19386  mndodcong  19460  cmn4  19719  ablsub4  19728  abladdsub4  19729  lsm4  19778  abvdom  20679  abvtrivd  20681  lspsnvs  20963  lspsneu  20972  lspfixed  20977  lspexch  20978  lsmcv  20990  lspsolvlem  20991  mvrf1  21883  coe1sclmulfv  22153  m1detdiag  22450  cnprest  23144  isreg2  23232  elptr  23428  hausflimlem  23834  trcfilu  24150  ssblps  24279  ssbl  24280  prdsxmslem2  24389  tgqioo  24667  metnrm  24729  bndth  24835  ncvspi  25035  cph2ass  25092  iscau3  25157  ovolunlem2  25378  dvres2  25792  dvfsumlem2  25912  dvfsumlem2OLD  25913  dvfsum2  25920  deg1tm  26005  plyadd  26102  plymul  26103  coeeu  26110  coemullem  26135  aalioulem4  26221  cxplea  26581  cxple2  26582  cxplt2  26583  cxple2a  26584  cxpcn3lem  26633  angcan  26685  ang180lem5  26696  divsqrtsumlem  26863  logexprlim  27109  dchrvmasumlema  27384  dchrisum0lema  27398  logdivsum  27417  log2sumbnd  27428  padicabv  27514  nolesgn2ores  27556  nogesgn1o  27557  nogesgn1ores  27558  nolt02o  27579  nogt01o  27580  nosupinfsep  27616  noetalem1  27625  noeta2  27668  scutbdaylt  27702  tghilberti2  28393  brbtwn2  28667  axcontlem4  28729  axcontlem8  28733  clwlkl1loop  29545  chscllem4  31398  mdslmd4i  32091  orngmul  32924  nexple  33537  measxun2  33738  measun  33739  mbfmco2  33794  probun  33948  satfv1fvfmla1  34942  wsuclem  35330  cgrcomim  35494  cgrcoml  35501  cgrcomr  35502  cgrdegen  35509  btwnintr  35524  btwnexch3  35525  btwnouttr  35529  btwnexch  35530  btwndiff  35532  ifscgr  35549  lineid  35588  btwnconn1lem7  35598  btwnconn1lem8  35599  btwnconn1lem9  35600  btwnconn1lem12  35603  midofsegid  35609  brsegle2  35614  btwnoutside  35630  outsideoftr  35634  cnres2  37142  heibor  37200  lsmsat  38389  lkrlsp  38483  lkrlsp2  38484  lkrlsp3  38485  lshpkrlem6  38496  latm4  38614  omlspjN  38642  hlatj4  38755  4noncolr3  38835  4noncolr2  38836  4noncolr1  38837  3dimlem3a  38842  3dimlem4a  38845  3dimlem4  38846  3dimlem4OLDN  38847  1cvratex  38855  hlatexch4  38863  3atlem4  38868  atcvrlln2  38901  atcvrlln  38902  llnmlplnN  38921  lplnnlelln  38925  lvoli2  38963  lvolnlelln  38966  lvolnlelpln  38967  4atlem11b  38990  4atlem12b  38993  2lplnj  39002  dalemzeo  39015  dath2  39119  lncvrat  39164  cdlemb  39176  elpaddri  39184  padd4N  39222  llnmod2i2  39245  llnexchb2  39251  dalawlem1  39253  dalawlem2  39254  osumcllem6N  39343  pexmidlem3N  39354  pexmidlem4N  39355  lhp2lt  39383  lhp2at0  39414  lhp2atne  39416  lhp2at0ne  39418  lhpmod2i2  39420  lhpmod6i1  39421  lhpat  39425  lhpat3  39428  4atexlemex6  39456  ltrncoval  39527  ltrncnv  39528  ltrnnidn  39556  cdlemd7  39586  cdleme0b  39594  cdleme0c  39595  cdleme0fN  39600  cdleme0ex1N  39605  cdleme7d  39628  cdleme7e  39629  cdleme7ga  39630  cdleme7  39631  cdleme11a  39642  cdleme17c  39670  cdleme22gb  39676  cdlemeda  39680  cdleme20k  39701  cdleme21a  39707  cdleme21at  39710  cdleme21d  39712  cdleme22f2  39729  cdleme22g  39730  cdleme24  39734  cdleme28  39755  cdlemefrs29cpre1  39780  cdlemefr29exN  39784  cdlemefr32sn2aw  39786  cdleme32fva  39819  cdleme32fva1  39820  cdleme35a  39830  cdleme42c  39854  cdleme42e  39861  cdleme42f  39862  cdleme42g  39863  cdleme42h  39864  cdleme43bN  39872  cdleme46f2g2  39875  cdleme17d2  39877  cdleme4gfv  39889  cdlemeg46c  39895  cdlemeg46nlpq  39899  cdlemeg46gfre  39914  cdlemeg49lebilem  39921  cdleme50trn1  39931  cdleme50trn2  39933  cdleme50ltrn  39939  cdleme  39942  cdlemf1  39943  cdlemf  39945  trlord  39951  ltrniotavalbN  39966  cdlemg1cex  39970  cdlemg2dN  39972  cdlemg2ce  39974  cdlemg2fvlem  39976  cdlemg2idN  39978  cdlemg2kq  39984  cdlemg2l  39985  cdlemg7fvN  40006  cdlemg7aN  40007  cdlemg8a  40009  cdlemg11aq  40020  cdlemg12d  40028  cdlemg13a  40033  cdlemg13  40034  cdlemg14f  40035  cdlemg14g  40036  cdlemg17b  40044  cdlemg27a  40074  cdlemg31b0N  40076  cdlemg31a  40079  cdlemg31b  40080  cdlemg31c  40081  ltrnco  40101  trlcoabs2N  40104  trlcocnvat  40106  trlconid  40107  trlcolem  40108  cdlemg42  40111  cdlemg43  40112  cdlemg47a  40116  cdlemg46  40117  cdlemg47  40118  tendoeq1  40146  tendocoval  40148  tendoco2  40150  tendoplco2  40161  tendopltp  40162  cdlemh1  40197  cdlemh2  40198  cdlemi1  40200  cdlemi  40202  cdlemk1  40213  cdlemk2  40214  cdlemk3  40215  cdlemk4  40216  cdlemk8  40220  cdlemk9  40221  cdlemk9bN  40222  cdlemk31  40278  cdlemk28-3  40290  cdlemk19xlem  40324  cdlemk39u  40350  cdlemk19u  40352  cdlemk56w  40355  cdlemn7  40585  cdlemn8  40586  cdlemn9  40587  dihordlem6  40595  dihordlem7  40596  dihordlem7b  40597  dihord1  40600  dihord2a  40601  dihord11c  40606  dihord2pre  40607  dihord2pre2  40608  dihlsscpre  40616  dihord4  40640  dihord6b  40642  dihmeetlem2N  40681  dihglbcpreN  40682  dihmeetcN  40684  dihmeetbclemN  40686  dihmeetlem3N  40687  dihmeetlem9N  40697  dihmeetlem13N  40701  dihmeetlem20N  40708  mapdpglem24  41086  mapdpglem32  41087  baerlem3lem2  41092  baerlem5alem2  41093  baerlem5blem2  41094  mapdh9aOLDN  41172  hdmap14lem6  41255  nnadddir  41722  sn-addlid  41836  mzpmfp  42044  mzpsubst  42045  pellexlem5  42130  pell14qrexpclnn0  42163  pellfundex  42183  qirropth  42205  monotuz  42239  congmul  42265  congsub  42268  mzpcong  42270  fzmaxdif  42279  jm2.15nn0  42301  idomsubgmo  42498  trclimalb2  43034  mnringmulrcld  43544  fourierdlem42  45418  fourierdlem48  45423  fourierdlem80  45455  prmdvdsfmtnof1lem1  46805  lidldomn1  47162  rngccatidALTV  47203  ringccatidALTV  47237  coe1sclmulval  47322  line2  47694  line2xlem  47695  line2x  47696  line2y  47697  itsclc0yqsol  47706  seposep  47813  iscnrm3rlem8  47835  iscnrm3llem2  47838