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  7292  uniinqs  7451  unxpdomlem3  7784  sup0  7986  fin23lem11  8745  reclem3pr  9473  dedekind  9796  addid2  9815  dmdcan  10316  xaddass2  11536  xlt2add  11546  xadddi2  11583  expaddzlem  12312  expaddz  12313  expmulz  12315  expdiv  12320  ccatopth2  12812  relexpaddnn  13093  o1add  13655  o1mul  13656  o1sub  13657  ntrivcvgmul  13936  prmexpb  14632  pcpremul  14747  pcdiv  14756  pcqmul  14757  pcqdiv  14761  4sqlem12  14854  f1ocpbllem  15372  ercpbl  15397  erlecpbl  15398  latjlej12  16255  latmlem12  16271  latj4  16289  symgsssg  17050  symgfisg  17051  mndodcong  17124  cmn4  17375  ablsub4  17381  abladdsub4  17382  lsm4  17424  abvdom  17992  abvtrivd  17994  lspsnvs  18263  lspsneu  18272  lspfixed  18277  lspexch  18278  lsmcv  18290  lspsolvlem  18291  mvrf1  18575  coe1sclmulfv  18802  m1detdiag  19544  cnprest  20227  isreg2  20315  elptr  20510  hausflimlem  20916  trcfilu  21231  ssblps  21359  ssbl  21360  prdsxmslem2  21466  tgqioo  21720  metnrm  21781  bndth  21873  cph2ass  22074  iscau3  22132  ovolunlem2  22320  dvres2  22735  dvfsumlem2  22847  dvfsum2  22854  deg1tm  22935  plyadd  23030  plymul  23031  coeeu  23038  coemullem  23063  aalioulem4  23147  cxplea  23497  cxple2  23498  cxplt2  23499  cxple2a  23500  cxpcn3lem  23543  angcan  23587  ang180lem5  23598  divsqrtsumlem  23761  logexprlim  24007  dchrvmasumlema  24192  dchrisum0lema  24206  logdivsum  24225  log2sumbnd  24236  padicabv  24322  tghilberti2  24533  brbtwn2  24772  axcontlem4  24834  axcontlem8  24838  1pthon  25157  chscllem4  27119  mdslmd4i  27812  orngmul  28396  nexple  28661  measxun2  28862  measun  28863  mbfmco2  28917  probun  29069  wsuclem  30286  cgrcomim  30532  cgrcoml  30539  cgrcomr  30540  cgrdegen  30547  btwnintr  30562  btwnexch3  30563  btwnouttr  30567  btwnexch  30568  btwndiff  30570  ifscgr  30587  lineid  30626  btwnconn1lem7  30636  btwnconn1lem8  30637  btwnconn1lem9  30638  btwnconn1lem12  30641  midofsegid  30647  brsegle2  30652  btwnoutside  30668  outsideoftr  30672  cnres2  31789  heibor  31847  lsmsat  32273  lkrlsp  32367  lkrlsp2  32368  lkrlsp3  32369  lshpkrlem6  32380  latm4  32498  omlspjN  32526  hlatj4  32638  4noncolr3  32717  4noncolr2  32718  4noncolr1  32719  3dimlem3a  32724  3dimlem4a  32727  3dimlem4  32728  3dimlem4OLDN  32729  1cvratex  32737  hlatexch4  32745  3atlem4  32750  atcvrlln2  32783  atcvrlln  32784  llnmlplnN  32803  lplnnlelln  32807  lvoli2  32845  lvolnlelln  32848  lvolnlelpln  32849  4atlem11b  32872  4atlem12b  32875  2lplnj  32884  dalemzeo  32897  dath2  33001  lncvrat  33046  cdlemb  33058  elpaddri  33066  padd4N  33104  llnmod2i2  33127  llnexchb2  33133  dalawlem1  33135  dalawlem2  33136  osumcllem6N  33225  pexmidlem3N  33236  pexmidlem4N  33237  lhp2lt  33265  lhp2at0  33296  lhp2atne  33298  lhp2at0ne  33300  lhpmod2i2  33302  lhpmod6i1  33303  lhpat  33307  lhpat3  33310  4atexlemex6  33338  ltrncoval  33409  ltrncnv  33410  ltrnnidn  33439  cdlemd7  33469  cdleme0b  33477  cdleme0c  33478  cdleme0fN  33483  cdleme0ex1N  33488  cdleme7d  33511  cdleme7e  33512  cdleme7ga  33513  cdleme7  33514  cdleme11a  33525  cdleme17c  33553  cdleme22gb  33559  cdlemeda  33563  cdleme20k  33585  cdleme21a  33591  cdleme21at  33594  cdleme21d  33596  cdleme22f2  33613  cdleme22g  33614  cdleme24  33618  cdleme28  33639  cdlemefrs29cpre1  33664  cdlemefr29exN  33668  cdlemefr32sn2aw  33670  cdleme32fva  33703  cdleme32fva1  33704  cdleme35a  33714  cdleme42c  33738  cdleme42e  33745  cdleme42f  33746  cdleme42g  33747  cdleme42h  33748  cdleme43bN  33756  cdleme46f2g2  33759  cdleme17d2  33761  cdleme4gfv  33773  cdlemeg46c  33779  cdlemeg46nlpq  33783  cdlemeg46gfre  33798  cdlemeg49lebilem  33805  cdleme50trn1  33815  cdleme50trn2  33817  cdleme50ltrn  33823  cdleme  33826  cdlemf1  33827  cdlemf  33829  trlord  33835  ltrniotavalbN  33850  cdlemg1cex  33854  cdlemg2dN  33856  cdlemg2ce  33858  cdlemg2fvlem  33860  cdlemg2idN  33862  cdlemg2kq  33868  cdlemg2l  33869  cdlemg7fvN  33890  cdlemg7aN  33891  cdlemg8a  33893  cdlemg11aq  33904  cdlemg12d  33912  cdlemg13a  33917  cdlemg13  33918  cdlemg14f  33919  cdlemg14g  33920  cdlemg17b  33928  cdlemg27a  33958  cdlemg31b0N  33960  cdlemg31a  33963  cdlemg31b  33964  cdlemg31c  33965  ltrnco  33985  trlcoabs2N  33988  trlcocnvat  33990  trlconid  33991  trlcolem  33992  cdlemg42  33995  cdlemg43  33996  cdlemg47a  34000  cdlemg46  34001  cdlemg47  34002  tendoeq1  34030  tendocoval  34032  tendoco2  34034  tendoplco2  34045  tendopltp  34046  cdlemh1  34081  cdlemh2  34082  cdlemi1  34084  cdlemi  34086  cdlemk1  34097  cdlemk2  34098  cdlemk3  34099  cdlemk4  34100  cdlemk8  34104  cdlemk9  34105  cdlemk9bN  34106  cdlemk31  34162  cdlemk28-3  34174  cdlemk19xlem  34208  cdlemk39u  34234  cdlemk19u  34236  cdlemk56w  34239  cdlemn7  34470  cdlemn8  34471  cdlemn9  34472  dihordlem6  34480  dihordlem7  34481  dihordlem7b  34482  dihord1  34485  dihord2a  34486  dihord11c  34491  dihord2pre  34492  dihord2pre2  34493  dihlsscpre  34501  dihord4  34525  dihord6b  34527  dihmeetlem2N  34566  dihglbcpreN  34567  dihmeetcN  34569  dihmeetbclemN  34571  dihmeetlem3N  34572  dihmeetlem9N  34582  dihmeetlem13N  34586  dihmeetlem20N  34593  mapdpglem24  34971  mapdpglem32  34972  baerlem3lem2  34977  baerlem5alem2  34978  baerlem5blem2  34979  mapdh9aOLDN  35058  hdmap14lem6  35143  mzpmfp  35288  mzpsubst  35289  pellexlem5  35377  pell14qrexpclnn0  35410  pellfundex  35430  qirropth  35452  monotuz  35485  expmordi  35491  congmul  35513  congsub  35516  mzpcong  35518  fzmaxdif  35527  jm2.15nn0  35554  idomsubgmo  35761  trclimalb2  35947  fourierdlem42  37570  fourierdlem48  37576  fourierdlem80  37608  lidldomn1  38669  rngccatidALTV  38739  ringccatidALTV  38802  coe1sclmulval  38927
  Copyright terms: Public domain W3C validator