MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  simp2r Structured version   Unicode version

Theorem simp2r 1032
Description: Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.)
Assertion
Ref Expression
simp2r  |-  ( (
ph  /\  ( ps  /\ 
ch )  /\  th )  ->  ch )

Proof of Theorem simp2r
StepHypRef Expression
1 simpr 462 . 2  |-  ( ( ps  /\  ch )  ->  ch )
213ad2ant2 1027 1  |-  ( (
ph  /\  ( ps  /\ 
ch )  /\  th )  ->  ch )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370    /\ w3a 982
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 188  df-an 372  df-3an 984
This theorem is referenced by:  simpl2r  1059  simpr2r  1065  simp12r  1119  simp22r  1125  simp32r  1131  funprg  5650  fsnunf  6117  f1oiso2  6258  fnsuppres  6953  omeulem2  7295  uniinqs  7454  unxpdomlem3  7787  sup0  7989  fin23lem11  8754  reclem3pr  9481  dedekind  9804  addid2  9823  dmdcan  10324  xaddass2  11543  xlt2add  11553  xadddi2  11590  expaddzlem  12321  expaddz  12322  expmulz  12324  expdiv  12329  ccatopth2  12829  relexpaddnn  13114  o1add  13676  o1mul  13677  o1sub  13678  ntrivcvgmul  13957  prmexpb  14669  pcpremul  14792  pcdiv  14801  pcqmul  14802  pcqdiv  14806  4sqlem12  14899  f1ocpbllem  15429  ercpbl  15454  erlecpbl  15455  latjlej12  16312  latmlem12  16328  latj4  16346  symgsssg  17107  symgfisg  17108  mndodcong  17190  cmn4  17448  ablsub4  17454  abladdsub4  17455  lsm4  17497  abvdom  18065  abvtrivd  18067  lspsnvs  18336  lspsneu  18345  lspfixed  18350  lspexch  18351  lsmcv  18363  lspsolvlem  18364  mvrf1  18648  coe1sclmulfv  18875  m1detdiag  19620  cnprest  20303  isreg2  20391  elptr  20586  hausflimlem  20992  trcfilu  21307  ssblps  21435  ssbl  21436  prdsxmslem2  21542  tgqioo  21816  metnrm  21892  bndth  21984  cph2ass  22188  iscau3  22246  ovolunlem2  22449  dvres2  22865  dvfsumlem2  22977  dvfsum2  22984  deg1tm  23065  plyadd  23169  plymul  23170  coeeu  23177  coemullem  23202  aalioulem4  23289  cxplea  23639  cxple2  23640  cxplt2  23641  cxple2a  23642  cxpcn3lem  23685  angcan  23729  ang180lem5  23740  divsqrtsumlem  23903  logexprlim  24151  dchrvmasumlema  24336  dchrisum0lema  24350  logdivsum  24369  log2sumbnd  24380  padicabv  24466  tghilberti2  24681  brbtwn2  24933  axcontlem4  24995  axcontlem8  24999  1pthon  25319  chscllem4  27291  mdslmd4i  27984  orngmul  28574  nexple  28839  measxun2  29040  measun  29041  mbfmco2  29095  probun  29260  wsuclem  30515  cgrcomim  30761  cgrcoml  30768  cgrcomr  30769  cgrdegen  30776  btwnintr  30791  btwnexch3  30792  btwnouttr  30796  btwnexch  30797  btwndiff  30799  ifscgr  30816  lineid  30855  btwnconn1lem7  30865  btwnconn1lem8  30866  btwnconn1lem9  30867  btwnconn1lem12  30870  midofsegid  30876  brsegle2  30881  btwnoutside  30897  outsideoftr  30901  cnres2  32059  heibor  32117  lsmsat  32543  lkrlsp  32637  lkrlsp2  32638  lkrlsp3  32639  lshpkrlem6  32650  latm4  32768  omlspjN  32796  hlatj4  32908  4noncolr3  32987  4noncolr2  32988  4noncolr1  32989  3dimlem3a  32994  3dimlem4a  32997  3dimlem4  32998  3dimlem4OLDN  32999  1cvratex  33007  hlatexch4  33015  3atlem4  33020  atcvrlln2  33053  atcvrlln  33054  llnmlplnN  33073  lplnnlelln  33077  lvoli2  33115  lvolnlelln  33118  lvolnlelpln  33119  4atlem11b  33142  4atlem12b  33145  2lplnj  33154  dalemzeo  33167  dath2  33271  lncvrat  33316  cdlemb  33328  elpaddri  33336  padd4N  33374  llnmod2i2  33397  llnexchb2  33403  dalawlem1  33405  dalawlem2  33406  osumcllem6N  33495  pexmidlem3N  33506  pexmidlem4N  33507  lhp2lt  33535  lhp2at0  33566  lhp2atne  33568  lhp2at0ne  33570  lhpmod2i2  33572  lhpmod6i1  33573  lhpat  33577  lhpat3  33580  4atexlemex6  33608  ltrncoval  33679  ltrncnv  33680  ltrnnidn  33709  cdlemd7  33739  cdleme0b  33747  cdleme0c  33748  cdleme0fN  33753  cdleme0ex1N  33758  cdleme7d  33781  cdleme7e  33782  cdleme7ga  33783  cdleme7  33784  cdleme11a  33795  cdleme17c  33823  cdleme22gb  33829  cdlemeda  33833  cdleme20k  33855  cdleme21a  33861  cdleme21at  33864  cdleme21d  33866  cdleme22f2  33883  cdleme22g  33884  cdleme24  33888  cdleme28  33909  cdlemefrs29cpre1  33934  cdlemefr29exN  33938  cdlemefr32sn2aw  33940  cdleme32fva  33973  cdleme32fva1  33974  cdleme35a  33984  cdleme42c  34008  cdleme42e  34015  cdleme42f  34016  cdleme42g  34017  cdleme42h  34018  cdleme43bN  34026  cdleme46f2g2  34029  cdleme17d2  34031  cdleme4gfv  34043  cdlemeg46c  34049  cdlemeg46nlpq  34053  cdlemeg46gfre  34068  cdlemeg49lebilem  34075  cdleme50trn1  34085  cdleme50trn2  34087  cdleme50ltrn  34093  cdleme  34096  cdlemf1  34097  cdlemf  34099  trlord  34105  ltrniotavalbN  34120  cdlemg1cex  34124  cdlemg2dN  34126  cdlemg2ce  34128  cdlemg2fvlem  34130  cdlemg2idN  34132  cdlemg2kq  34138  cdlemg2l  34139  cdlemg7fvN  34160  cdlemg7aN  34161  cdlemg8a  34163  cdlemg11aq  34174  cdlemg12d  34182  cdlemg13a  34187  cdlemg13  34188  cdlemg14f  34189  cdlemg14g  34190  cdlemg17b  34198  cdlemg27a  34228  cdlemg31b0N  34230  cdlemg31a  34233  cdlemg31b  34234  cdlemg31c  34235  ltrnco  34255  trlcoabs2N  34258  trlcocnvat  34260  trlconid  34261  trlcolem  34262  cdlemg42  34265  cdlemg43  34266  cdlemg47a  34270  cdlemg46  34271  cdlemg47  34272  tendoeq1  34300  tendocoval  34302  tendoco2  34304  tendoplco2  34315  tendopltp  34316  cdlemh1  34351  cdlemh2  34352  cdlemi1  34354  cdlemi  34356  cdlemk1  34367  cdlemk2  34368  cdlemk3  34369  cdlemk4  34370  cdlemk8  34374  cdlemk9  34375  cdlemk9bN  34376  cdlemk31  34432  cdlemk28-3  34444  cdlemk19xlem  34478  cdlemk39u  34504  cdlemk19u  34506  cdlemk56w  34509  cdlemn7  34740  cdlemn8  34741  cdlemn9  34742  dihordlem6  34750  dihordlem7  34751  dihordlem7b  34752  dihord1  34755  dihord2a  34756  dihord11c  34761  dihord2pre  34762  dihord2pre2  34763  dihlsscpre  34771  dihord4  34795  dihord6b  34797  dihmeetlem2N  34836  dihglbcpreN  34837  dihmeetcN  34839  dihmeetbclemN  34841  dihmeetlem3N  34842  dihmeetlem9N  34852  dihmeetlem13N  34856  dihmeetlem20N  34863  mapdpglem24  35241  mapdpglem32  35242  baerlem3lem2  35247  baerlem5alem2  35248  baerlem5blem2  35249  mapdh9aOLDN  35328  hdmap14lem6  35413  mzpmfp  35558  mzpsubst  35559  pellexlem5  35647  pell14qrexpclnn0  35682  pellfundex  35704  qirropth  35726  monotuz  35759  expmordi  35765  congmul  35787  congsub  35790  mzpcong  35792  fzmaxdif  35801  jm2.15nn0  35828  idomsubgmo  36042  trclimalb2  36288  fourierdlem42  37952  fourierdlem42OLD  37953  fourierdlem48  37958  fourierdlem80  37990  lidldomn1  39541  rngccatidALTV  39611  ringccatidALTV  39674  coe1sclmulval  39799
  Copyright terms: Public domain W3C validator