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

Syntax hints:   → wi 4   ∧ wa 394   ∧ 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 395  df-3an 1086

This theorem is referenced by:  simp12r  1284  simp22r  1290  simp32r  1296  fsnunf  7191  f1oiso2  7356  fnsuppres  8197  frrlem4  8296  omeulem2  8605  uniinqs  8818  unxpdomlem3  9279  sup0  9502  fin23lem11  10351  reclem3pr  11083  dedekind  11418  addlid  11438  subaddmulsub  11718  dmdcan  11969  xaddass2  13277  xlt2add  13287  xadddi2  13324  expaddzlem  14119  expaddz  14120  expmulz  14122  expdiv  14127  expmordi  14180  pfxeq  14699  ccatopth2  14720  relexpaddnn  15051  o1add  15611  o1mul  15612  o1sub  15613  ntrivcvgmul  15901  prmexpb  16716  pcpremul  16840  pcdiv  16849  pcqmul  16850  pcqdiv  16854  4sqlem12  16953  f1ocpbllem  17534  ercpbl  17559  erlecpbl  17560  latjlej12  18475  latmlem12  18491  latj4  18509  gsumsgrpccat  18825  symgsssg  19461  symgfisg  19462  mndodcong  19536  cmn4  19795  ablsub4  19804  abladdsub4  19805  lsm4  19854  abvdom  20805  abvtrivd  20807  lspsnvs  21091  lspsneu  21100  lspfixed  21105  lspexch  21106  lsmcv  21118  lspsolvlem  21119  mvrf1  21991  coe1sclmulfv  22270  m1detdiag  22587  cnprest  23281  isreg2  23369  elptr  23565  hausflimlem  23971  trcfilu  24287  ssblps  24416  ssbl  24417  prdsxmslem2  24526  tgqioo  24804  metnrm  24866  bndth  24972  ncvspi  25172  cph2ass  25229  iscau3  25294  ovolunlem2  25515  dvres2  25929  dvfsumlem2  26049  dvfsumlem2OLD  26050  dvfsum2  26057  deg1tm  26143  plyadd  26241  plymul  26242  coeeu  26249  coemullem  26274  aalioulem4  26360  cxplea  26720  cxple2  26721  cxplt2  26722  cxple2a  26723  cxpcn3lem  26772  angcan  26827  ang180lem5  26838  divsqrtsumlem  27005  logexprlim  27251  dchrvmasumlema  27526  dchrisum0lema  27540  logdivsum  27559  log2sumbnd  27570  padicabv  27656  nolesgn2ores  27699  nogesgn1o  27700  nogesgn1ores  27701  nolt02o  27722  nogt01o  27723  nosupinfsep  27759  noetalem1  27768  noeta2  27811  scutbdaylt  27845  tghilberti2  28562  brbtwn2  28836  axcontlem4  28898  axcontlem8  28902  clwlkl1loop  29717  chscllem4  31570  mdslmd4i  32263  orngmul  33186  nexple  33855  measxun2  34056  measun  34057  mbfmco2  34112  probun  34266  satfv1fvfmla1  35264  wsuclem  35662  cgrcomim  35826  cgrcoml  35833  cgrcomr  35834  cgrdegen  35841  btwnintr  35856  btwnexch3  35857  btwnouttr  35861  btwnexch  35862  btwndiff  35864  ifscgr  35881  lineid  35920  btwnconn1lem7  35930  btwnconn1lem8  35931  btwnconn1lem9  35932  btwnconn1lem12  35935  midofsegid  35941  brsegle2  35946  btwnoutside  35962  outsideoftr  35966  cnres2  37477  heibor  37535  lsmsat  38719  lkrlsp  38813  lkrlsp2  38814  lkrlsp3  38815  lshpkrlem6  38826  latm4  38944  omlspjN  38972  hlatj4  39085  4noncolr3  39165  4noncolr2  39166  4noncolr1  39167  3dimlem3a  39172  3dimlem4a  39175  3dimlem4  39176  3dimlem4OLDN  39177  1cvratex  39185  hlatexch4  39193  3atlem4  39198  atcvrlln2  39231  atcvrlln  39232  llnmlplnN  39251  lplnnlelln  39255  lvoli2  39293  lvolnlelln  39296  lvolnlelpln  39297  4atlem11b  39320  4atlem12b  39323  2lplnj  39332  dalemzeo  39345  dath2  39449  lncvrat  39494  cdlemb  39506  elpaddri  39514  padd4N  39552  llnmod2i2  39575  llnexchb2  39581  dalawlem1  39583  dalawlem2  39584  osumcllem6N  39673  pexmidlem3N  39684  pexmidlem4N  39685  lhp2lt  39713  lhp2at0  39744  lhp2atne  39746  lhp2at0ne  39748  lhpmod2i2  39750  lhpmod6i1  39751  lhpat  39755  lhpat3  39758  4atexlemex6  39786  ltrncoval  39857  ltrncnv  39858  ltrnnidn  39886  cdlemd7  39916  cdleme0b  39924  cdleme0c  39925  cdleme0fN  39930  cdleme0ex1N  39935  cdleme7d  39958  cdleme7e  39959  cdleme7ga  39960  cdleme7  39961  cdleme11a  39972  cdleme17c  40000  cdleme22gb  40006  cdlemeda  40010  cdleme20k  40031  cdleme21a  40037  cdleme21at  40040  cdleme21d  40042  cdleme22f2  40059  cdleme22g  40060  cdleme24  40064  cdleme28  40085  cdlemefrs29cpre1  40110  cdlemefr29exN  40114  cdlemefr32sn2aw  40116  cdleme32fva  40149  cdleme32fva1  40150  cdleme35a  40160  cdleme42c  40184  cdleme42e  40191  cdleme42f  40192  cdleme42g  40193  cdleme42h  40194  cdleme43bN  40202  cdleme46f2g2  40205  cdleme17d2  40207  cdleme4gfv  40219  cdlemeg46c  40225  cdlemeg46nlpq  40229  cdlemeg46gfre  40244  cdlemeg49lebilem  40251  cdleme50trn1  40261  cdleme50trn2  40263  cdleme50ltrn  40269  cdleme  40272  cdlemf1  40273  cdlemf  40275  trlord  40281  ltrniotavalbN  40296  cdlemg1cex  40300  cdlemg2dN  40302  cdlemg2ce  40304  cdlemg2fvlem  40306  cdlemg2idN  40308  cdlemg2kq  40314  cdlemg2l  40315  cdlemg7fvN  40336  cdlemg7aN  40337  cdlemg8a  40339  cdlemg11aq  40350  cdlemg12d  40358  cdlemg13a  40363  cdlemg13  40364  cdlemg14f  40365  cdlemg14g  40366  cdlemg17b  40374  cdlemg27a  40404  cdlemg31b0N  40406  cdlemg31a  40409  cdlemg31b  40410  cdlemg31c  40411  ltrnco  40431  trlcoabs2N  40434  trlcocnvat  40436  trlconid  40437  trlcolem  40438  cdlemg42  40441  cdlemg43  40442  cdlemg47a  40446  cdlemg46  40447  cdlemg47  40448  tendoeq1  40476  tendocoval  40478  tendoco2  40480  tendoplco2  40491  tendopltp  40492  cdlemh1  40527  cdlemh2  40528  cdlemi1  40530  cdlemi  40532  cdlemk1  40543  cdlemk2  40544  cdlemk3  40545  cdlemk4  40546  cdlemk8  40550  cdlemk9  40551  cdlemk9bN  40552  cdlemk31  40608  cdlemk28-3  40620  cdlemk19xlem  40654  cdlemk39u  40680  cdlemk19u  40682  cdlemk56w  40685  cdlemn7  40915  cdlemn8  40916  cdlemn9  40917  dihordlem6  40925  dihordlem7  40926  dihordlem7b  40927  dihord1  40930  dihord2a  40931  dihord11c  40936  dihord2pre  40937  dihord2pre2  40938  dihlsscpre  40946  dihord4  40970  dihord6b  40972  dihmeetlem2N  41011  dihglbcpreN  41012  dihmeetcN  41014  dihmeetbclemN  41016  dihmeetlem3N  41017  dihmeetlem9N  41027  dihmeetlem13N  41031  dihmeetlem20N  41038  mapdpglem24  41416  mapdpglem32  41417  baerlem3lem2  41422  baerlem5alem2  41423  baerlem5blem2  41424  mapdh9aOLDN  41502  hdmap14lem6  41585  nnadddir  42009  sn-addlid  42115  mzpmfp  42441  mzpsubst  42442  pellexlem5  42527  pell14qrexpclnn0  42560  pellfundex  42580  qirropth  42602  monotuz  42636  congmul  42662  congsub  42665  mzpcong  42667  fzmaxdif  42676  jm2.15nn0  42698  idomsubgmo  42895  trclimalb2  43430  mnringmulrcld  43939  fourierdlem42  45806  fourierdlem48  45811  fourierdlem80  45843  prmdvdsfmtnof1lem1  47192  lidldomn1  47644  rngccatidALTV  47685  ringccatidALTV  47719  coe1sclmulval  47804  line2  48176  line2xlem  48177  line2x  48178  line2y  48179  itsclc0yqsol  48188  seposep  48295  iscnrm3rlem8  48317  iscnrm3llem2  48320