Theorem simp2r 1202

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

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

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 1089

This theorem is referenced by:  simp12r  1289  simp22r  1295  simp32r  1301  fsnunf  7133  f1oiso2  7300  fnsuppres  8134  frrlem4  8232  omeulem2  8511  uniinqs  8737  unxpdomlem3  9161  sup0  9373  fin23lem11  10230  reclem3pr  10963  dedekind  11300  addlid  11320  subaddmulsub  11604  dmdcan  11856  nnadddir  12224  xaddass2  13193  xlt2add  13203  xadddi2  13240  expaddzlem  14058  expaddz  14059  expmulz  14061  expdiv  14066  expmordi  14120  pfxeq  14649  ccatopth2  14670  relexpaddnn  15004  o1add  15567  o1mul  15568  o1sub  15569  ntrivcvgmul  15858  prmexpb  16680  pcpremul  16805  pcdiv  16814  pcqmul  16815  pcqdiv  16819  4sqlem12  16918  f1ocpbllem  17479  ercpbl  17504  erlecpbl  17505  latjlej12  18412  latmlem12  18428  latj4  18446  gsumsgrpccat  18799  symgsssg  19433  symgfisg  19434  mndodcong  19508  cmn4  19767  ablsub4  19776  abladdsub4  19777  lsm4  19826  abvdom  20798  abvtrivd  20800  orngmul  20833  lspsnvs  21104  lspsneu  21113  lspfixed  21118  lspexch  21119  lsmcv  21131  lspsolvlem  21132  mvrf1  21974  coe1sclmulfv  22258  m1detdiag  22572  cnprest  23264  isreg2  23352  elptr  23548  hausflimlem  23954  trcfilu  24268  ssblps  24397  ssbl  24398  prdsxmslem2  24504  tgqioo  24775  metnrm  24838  bndth  24935  ncvspi  25133  cph2ass  25190  iscau3  25255  ovolunlem2  25475  dvres2  25889  dvfsumlem2  26004  dvfsum2  26011  deg1tm  26094  plyadd  26192  plymul  26193  coeeu  26200  coemullem  26225  aalioulem4  26312  cxplea  26673  cxple2  26674  cxplt2  26675  cxple2a  26676  cxpcn3lem  26724  angcan  26779  ang180lem5  26790  divsqrtsumlem  26957  logexprlim  27202  dchrvmasumlema  27477  dchrisum0lema  27491  logdivsum  27510  log2sumbnd  27521  padicabv  27607  nolesgn2ores  27650  nogesgn1o  27651  nogesgn1ores  27652  nolt02o  27673  nogt01o  27674  nosupinfsep  27710  noetalem1  27719  noeta2  27767  cutbdaylt  27804  expsgt0  28443  bdayfinbndlem1  28473  tghilberti2  28720  brbtwn2  28988  axcontlem4  29050  axcontlem8  29054  clwlkl1loop  29866  chscllem4  31726  mdslmd4i  32419  nexple  32932  measxun2  34370  measun  34371  mbfmco2  34425  probun  34579  satfv1fvfmla1  35621  wsuclem  36021  cgrcomim  36187  cgrcoml  36194  cgrcomr  36195  cgrdegen  36202  btwnintr  36217  btwnexch3  36218  btwnouttr  36222  btwnexch  36223  btwndiff  36225  ifscgr  36242  lineid  36281  btwnconn1lem7  36291  btwnconn1lem8  36292  btwnconn1lem9  36293  btwnconn1lem12  36296  midofsegid  36302  brsegle2  36307  btwnoutside  36323  outsideoftr  36327  ttcmin  36694  cnres2  38098  heibor  38156  lsmsat  39468  lkrlsp  39562  lkrlsp2  39563  lkrlsp3  39564  lshpkrlem6  39575  latm4  39693  omlspjN  39721  hlatj4  39834  4noncolr3  39913  4noncolr2  39914  4noncolr1  39915  3dimlem3a  39920  3dimlem4a  39923  3dimlem4  39924  3dimlem4OLDN  39925  1cvratex  39933  hlatexch4  39941  3atlem4  39946  atcvrlln2  39979  atcvrlln  39980  llnmlplnN  39999  lplnnlelln  40003  lvoli2  40041  lvolnlelln  40044  lvolnlelpln  40045  4atlem11b  40068  4atlem12b  40071  2lplnj  40080  dalemzeo  40093  dath2  40197  lncvrat  40242  cdlemb  40254  elpaddri  40262  padd4N  40300  llnmod2i2  40323  llnexchb2  40329  dalawlem1  40331  dalawlem2  40332  osumcllem6N  40421  pexmidlem3N  40432  pexmidlem4N  40433  lhp2lt  40461  lhp2at0  40492  lhp2atne  40494  lhp2at0ne  40496  lhpmod2i2  40498  lhpmod6i1  40499  lhpat  40503  lhpat3  40506  4atexlemex6  40534  ltrncoval  40605  ltrncnv  40606  ltrnnidn  40634  cdlemd7  40664  cdleme0b  40672  cdleme0c  40673  cdleme0fN  40678  cdleme0ex1N  40683  cdleme7d  40706  cdleme7e  40707  cdleme7ga  40708  cdleme7  40709  cdleme11a  40720  cdleme17c  40748  cdleme22gb  40754  cdlemeda  40758  cdleme20k  40779  cdleme21a  40785  cdleme21at  40788  cdleme21d  40790  cdleme22f2  40807  cdleme22g  40808  cdleme24  40812  cdleme28  40833  cdlemefrs29cpre1  40858  cdlemefr29exN  40862  cdlemefr32sn2aw  40864  cdleme32fva  40897  cdleme32fva1  40898  cdleme35a  40908  cdleme42c  40932  cdleme42e  40939  cdleme42f  40940  cdleme42g  40941  cdleme42h  40942  cdleme43bN  40950  cdleme46f2g2  40953  cdleme17d2  40955  cdleme4gfv  40967  cdlemeg46c  40973  cdlemeg46nlpq  40977  cdlemeg46gfre  40992  cdlemeg49lebilem  40999  cdleme50trn1  41009  cdleme50trn2  41011  cdleme50ltrn  41017  cdleme  41020  cdlemf1  41021  cdlemf  41023  trlord  41029  ltrniotavalbN  41044  cdlemg1cex  41048  cdlemg2dN  41050  cdlemg2ce  41052  cdlemg2fvlem  41054  cdlemg2idN  41056  cdlemg2kq  41062  cdlemg2l  41063  cdlemg7fvN  41084  cdlemg7aN  41085  cdlemg8a  41087  cdlemg11aq  41098  cdlemg12d  41106  cdlemg13a  41111  cdlemg13  41112  cdlemg14f  41113  cdlemg14g  41114  cdlemg17b  41122  cdlemg27a  41152  cdlemg31b0N  41154  cdlemg31a  41157  cdlemg31b  41158  cdlemg31c  41159  ltrnco  41179  trlcoabs2N  41182  trlcocnvat  41184  trlconid  41185  trlcolem  41186  cdlemg42  41189  cdlemg43  41190  cdlemg47a  41194  cdlemg46  41195  cdlemg47  41196  tendoeq1  41224  tendocoval  41226  tendoco2  41228  tendoplco2  41239  tendopltp  41240  cdlemh1  41275  cdlemh2  41276  cdlemi1  41278  cdlemi  41280  cdlemk1  41291  cdlemk2  41292  cdlemk3  41293  cdlemk4  41294  cdlemk8  41298  cdlemk9  41299  cdlemk9bN  41300  cdlemk31  41356  cdlemk28-3  41368  cdlemk19xlem  41402  cdlemk39u  41428  cdlemk19u  41430  cdlemk56w  41433  cdlemn7  41663  cdlemn8  41664  cdlemn9  41665  dihordlem6  41673  dihordlem7  41674  dihordlem7b  41675  dihord1  41678  dihord2a  41679  dihord11c  41684  dihord2pre  41685  dihord2pre2  41686  dihlsscpre  41694  dihord4  41718  dihord6b  41720  dihmeetlem2N  41759  dihglbcpreN  41760  dihmeetcN  41762  dihmeetbclemN  41764  dihmeetlem3N  41765  dihmeetlem9N  41775  dihmeetlem13N  41779  dihmeetlem20N  41786  mapdpglem24  42164  mapdpglem32  42165  baerlem3lem2  42170  baerlem5alem2  42171  baerlem5blem2  42172  mapdh9aOLDN  42250  hdmap14lem6  42333  sn-addlid  42850  mzpmfp  43193  mzpsubst  43194  pellexlem5  43279  pell14qrexpclnn0  43312  pellfundex  43332  qirropth  43354  monotuz  43387  congmul  43413  congsub  43416  mzpcong  43418  fzmaxdif  43427  jm2.15nn0  43449  idomsubgmo  43639  trclimalb2  44171  mnringmulrcld  44673  fourierdlem42  46595  fourierdlem48  46600  fourierdlem80  46632  prmdvdsfmtnof1lem1  48059  cycldlenngric  48416  gpgedgvtx1  48550  lidldomn1  48719  rngccatidALTV  48760  ringccatidALTV  48794  coe1sclmulval  48873  line2  49240  line2xlem  49241  line2x  49242  line2y  49243  itsclc0yqsol  49252  seposep  49413  iscnrm3rlem8  49434  iscnrm3llem2  49437