Theorem simp2r 1219

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  simp12r  1306  simp22r  1312  simp32r  1318  fsnunf  7187  f1resrcmplf1d  7276  f1oiso2  7357  fnsuppres  8193  frrlem4  8292  omeulem2  8574  uniinqs  8801  unxpdomlem3  9232  sup0  9441  fin23lem11  10323  reclem3pr  11062  dedekind  11401  addlid  11421  subaddmulsub  11705  dmdcan  11953  nnadddir  12320  xaddass2  13306  xlt2add  13316  xadddi2  13353  expaddzlem  14173  expaddz  14174  expmulz  14176  expdiv  14181  expmordi  14235  pfxeq  14769  ccatopth2  14790  relexpaddnn  15128  o1add  15705  o1mul  15706  o1sub  15707  ntrivcvgmul  15995  prmexpb  16816  pcpremul  16941  pcdiv  16950  pcqmul  16951  pcqdiv  16955  4sqlem12  17054  f1ocpbllem  17616  ercpbl  17641  erlecpbl  17642  latjlej12  18549  latmlem12  18565  latj4  18583  gsumsgrpccat  18955  symgsssg  19600  symgfisg  19601  mndodcong  19675  cmn4  19934  ablsub4  19943  abladdsub4  19944  lsm4  19993  abvdom  21002  abvtrivd  21004  orngmul  21037  lspsnvs  21307  lspsneu  21316  lspfixed  21321  lspexch  21322  lsmcv  21334  lspsolvlem  21335  mvrf1  22206  coe1sclmulfv  22515  m1detdiag  22825  cnprest  23520  isreg2  23608  elptr  23805  hausflimlem  24211  trcfilu  24525  ssblps  24654  ssbl  24655  prdsxmslem2  24761  tgqioo  25032  metnrm  25095  bndth  25192  ncvspi  25390  cph2ass  25447  iscau3  25512  ovolunlem2  25732  dvres2  26146  dvfsumlem2  26261  dvfsum2  26268  deg1tm  26351  plyadd  26450  plymul  26451  coeeu  26458  coemullem  26483  aalioulem4  26578  cxplea  26941  cxple2  26942  cxplt2  26943  cxple2a  26944  cxpcn3lem  26992  angcan  27047  ang180lem5  27058  divsqrtsumlem  27224  logexprlim  27469  dchrvmasumlema  27744  dchrisum0lema  27758  logdivsum  27777  log2sumbnd  27788  padicabv  27874  nolesgn2ores  27916  nogesgn1o  27917  nogesgn1ores  27918  nolt02o  27939  nogt01o  27940  nosupinfsep  27976  noetalem1  27985  noeta2  28034  cutbdaylt  28071  expsgt0  28710  bdayfinbndlem1  28740  tghilberti2  28993  brbtwn2  29370  axcontlem4  29432  axcontlem8  29436  clwlkl1loop  30257  umgr2cycllem  30633  chscllem4  32129  mdslmd4i  32822  nexple  33311  measxun2  34729  measun  34730  mbfmco2  34784  probun  34938  satfv1fvfmla1  36010  wsuclem  36410  cgrcomim  36577  cgrcoml  36584  cgrcomr  36585  cgrdegen  36592  btwnintr  36607  btwnexch3  36608  btwnouttr  36612  btwnexch  36613  btwndiff  36615  ifscgr  36632  lineid  36671  btwnconn1lem7  36681  btwnconn1lem8  36682  btwnconn1lem9  36683  btwnconn1lem12  36686  midofsegid  36692  brsegle2  36697  btwnoutside  36713  outsideoftr  36717  ttcmin  37123  cnres2  38521  heibor  38579  lsmsat  39889  lkrlsp  39983  lkrlsp2  39984  lkrlsp3  39985  lshpkrlem6  39996  latm4  40114  omlspjN  40142  hlatj4  40255  4noncolr3  40334  4noncolr2  40335  4noncolr1  40336  3dimlem3a  40341  3dimlem4a  40344  3dimlem4  40345  3dimlem4OLDN  40346  1cvratex  40354  hlatexch4  40362  3atlem4  40367  atcvrlln2  40400  atcvrlln  40401  llnmlplnN  40420  lplnnlelln  40424  lvoli2  40462  lvolnlelln  40465  lvolnlelpln  40466  4atlem11b  40489  4atlem12b  40492  2lplnj  40501  dalemzeo  40514  dath2  40618  lncvrat  40663  cdlemb  40675  elpaddri  40683  padd4N  40721  llnmod2i2  40744  llnexchb2  40750  dalawlem1  40752  dalawlem2  40753  osumcllem6N  40842  pexmidlem3N  40853  pexmidlem4N  40854  lhp2lt  40882  lhp2at0  40913  lhp2atne  40915  lhp2at0ne  40917  lhpmod2i2  40919  lhpmod6i1  40920  lhpat  40924  lhpat3  40927  4atexlemex6  40955  ltrncoval  41026  ltrncnv  41027  ltrnnidn  41055  cdlemd7  41085  cdleme0b  41093  cdleme0c  41094  cdleme0fN  41099  cdleme0ex1N  41104  cdleme7d  41127  cdleme7e  41128  cdleme7ga  41129  cdleme7  41130  cdleme11a  41141  cdleme17c  41169  cdleme22gb  41175  cdlemeda  41179  cdleme20k  41200  cdleme21a  41206  cdleme21at  41209  cdleme21d  41211  cdleme22f2  41228  cdleme22g  41229  cdleme24  41233  cdleme28  41254  cdlemefrs29cpre1  41279  cdlemefr29exN  41283  cdlemefr32sn2aw  41285  cdleme32fva  41318  cdleme32fva1  41319  cdleme35a  41329  cdleme42c  41353  cdleme42e  41360  cdleme42f  41361  cdleme42g  41362  cdleme42h  41363  cdleme43bN  41371  cdleme46f2g2  41374  cdleme17d2  41376  cdleme4gfv  41388  cdlemeg46c  41394  cdlemeg46nlpq  41398  cdlemeg46gfre  41413  cdlemeg49lebilem  41420  cdleme50trn1  41430  cdleme50trn2  41432  cdleme50ltrn  41438  cdleme  41441  cdlemf1  41442  cdlemf  41444  trlord  41450  ltrniotavalbN  41465  cdlemg1cex  41469  cdlemg2dN  41471  cdlemg2ce  41473  cdlemg2fvlem  41475  cdlemg2idN  41477  cdlemg2kq  41483  cdlemg2l  41484  cdlemg7fvN  41505  cdlemg7aN  41506  cdlemg8a  41508  cdlemg11aq  41519  cdlemg12d  41527  cdlemg13a  41532  cdlemg13  41533  cdlemg14f  41534  cdlemg14g  41535  cdlemg17b  41543  cdlemg27a  41573  cdlemg31b0N  41575  cdlemg31a  41578  cdlemg31b  41579  cdlemg31c  41580  ltrnco  41600  trlcoabs2N  41603  trlcocnvat  41605  trlconid  41606  trlcolem  41607  cdlemg42  41610  cdlemg43  41611  cdlemg47a  41615  cdlemg46  41616  cdlemg47  41617  tendoeq1  41645  tendocoval  41647  tendoco2  41649  tendoplco2  41660  tendopltp  41661  cdlemh1  41696  cdlemh2  41697  cdlemi1  41699  cdlemi  41701  cdlemk1  41712  cdlemk2  41713  cdlemk3  41714  cdlemk4  41715  cdlemk8  41719  cdlemk9  41720  cdlemk9bN  41721  cdlemk31  41777  cdlemk28-3  41789  cdlemk19xlem  41823  cdlemk39u  41849  cdlemk19u  41851  cdlemk56w  41854  cdlemn7  42084  cdlemn8  42085  cdlemn9  42086  dihordlem6  42094  dihordlem7  42095  dihordlem7b  42096  dihord1  42099  dihord2a  42100  dihord11c  42105  dihord2pre  42106  dihord2pre2  42107  dihlsscpre  42115  dihord4  42139  dihord6b  42141  dihmeetlem2N  42180  dihglbcpreN  42181  dihmeetcN  42183  dihmeetbclemN  42185  dihmeetlem3N  42186  dihmeetlem9N  42196  dihmeetlem13N  42200  dihmeetlem20N  42207  mapdpglem24  42585  mapdpglem32  42586  baerlem3lem2  42591  baerlem5alem2  42592  baerlem5blem2  42593  mapdh9aOLDN  42671  hdmap14lem6  42754  sn-addlid  43287  mzpmfp  43600  mzpsubst  43601  pellexlem5  43682  pell14qrexpclnn0  43715  pellfundex  43735  qirropth  43757  monotuz  43790  congmul  43816  congsub  43819  mzpcong  43821  fzmaxdif  43830  jm2.15nn0  43852  idomsubgmo  44042  trclimalb2  44574  mnringmulrcld  45074  fourierdlem42  46985  fourierdlem48  46990  fourierdlem80  47022  prmdvdsfmtnof1lem1  48495  cycldlenngric  48852  gpgedgvtx1  48986  lidldomn1  49154  rngccatidALTV  49195  ringccatidALTV  49229  coe1sclmulval  49323  line2  49690  line2xlem  49691  line2x  49692  line2y  49693  itsclc0yqsol  49702  seposep  49860  iscnrm3rlem8  49881  iscnrm3llem2  49884