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

Theorem simp2r 984
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 448 . 2  |-  ( ( ps  /\  ch )  ->  ch )
213ad2ant2 979 1  |-  ( (
ph  /\  ( ps  /\ 
ch )  /\  th )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    /\ w3a 936
This theorem is referenced by:  simpl2r  1011  simpr2r  1017  simp12r  1071  simp22r  1077  simp32r  1083  funprg  5459  fsnunf  5890  f1oiso2  6031  omeulem2  6785  uniinqs  6943  unxpdomlem3  7274  fin23lem11  8153  reclem3pr  8882  addid2  9205  dmdcan  9680  xaddass2  10785  xlt2add  10795  xadddi2  10832  expaddzlem  11378  expaddz  11379  expmulz  11381  expdiv  11385  ccatopth2  11732  o1add  12362  o1mul  12363  o1sub  12364  prmexpb  13072  pcpremul  13172  pcdiv  13181  pcqmul  13182  pcqdiv  13186  4sqlem12  13279  f1ocpbllem  13704  ercpbl  13729  erlecpbl  13730  latjlej12  14451  latmlem12  14467  latj4  14485  mndodcong  15135  cmn4  15386  ablsub4  15392  abladdsub4  15393  lsm4  15430  abvdom  15881  abvtrivd  15883  lspsnvs  16141  lspsneu  16150  lspfixed  16155  lspexch  16156  lsmcv  16168  lspsolvlem  16169  mvrf1  16444  coe1sclmulfv  16630  cnprest  17307  isreg2  17395  elptr  17558  hausflimlem  17964  trcfilu  18277  ssblps  18405  ssbl  18406  prdsxmslem2  18512  tgqioo  18784  metnrm  18845  bndth  18936  cph2ass  19128  iscau3  19184  ovolunlem2  19347  dvres2  19752  dvfsumlem2  19864  dvfsum2  19871  deg1tm  19994  plyadd  20089  plymul  20090  coeeu  20097  coemullem  20121  aalioulem4  20205  cxplea  20540  cxple2  20541  cxplt2  20542  cxple2a  20543  cxpcn3lem  20584  angcan  20597  ang180lem5  20608  divsqrsumlem  20771  logexprlim  20962  dchrvmasumlema  21147  dchrisum0lema  21161  logdivsum  21180  log2sumbnd  21191  padicabv  21277  1pthon  21544  chscllem4  23095  mdslmd4i  23789  ofldmul  24192  measxun2  24517  measun  24518  mbfmco2  24568  probun  24630  dedekind  25140  ntrivcvgmul  25183  brbtwn2  25748  axcontlem4  25810  axcontlem8  25814  cgrcomim  25827  cgrcoml  25834  cgrcomr  25835  cgrdegen  25842  btwnintr  25857  btwnexch3  25858  btwnouttr  25862  btwnexch  25863  btwndiff  25865  ifscgr  25882  lineid  25921  btwnconn1lem7  25931  btwnconn1lem8  25932  btwnconn1lem9  25933  btwnconn1lem12  25936  midofsegid  25942  brsegle2  25947  btwnoutside  25963  outsideoftr  25967  cnres2  26362  heibor  26420  mzpmfp  26694  mzpsubst  26695  pellexlem5  26786  pell14qrexpclnn0  26819  pellfundex  26839  qirropth  26861  monotuz  26894  expmordi  26900  congmul  26922  congsub  26925  mzpcong  26927  fzmaxdif  26936  jm2.15nn0  26964  symgsssg  27276  symgfisg  27277  idomsubgmo  27382  lsmsat  29491  lkrlsp  29585  lkrlsp2  29586  lkrlsp3  29587  lshpkrlem6  29598  latm4  29716  omlspjN  29744  hlatj4  29856  4noncolr3  29935  4noncolr2  29936  4noncolr1  29937  3dimlem3a  29942  3dimlem4a  29945  3dimlem4  29946  3dimlem4OLDN  29947  1cvratex  29955  hlatexch4  29963  3atlem4  29968  atcvrlln2  30001  atcvrlln  30002  llnmlplnN  30021  lplnnlelln  30025  lvoli2  30063  lvolnlelln  30066  lvolnlelpln  30067  4atlem11b  30090  4atlem12b  30093  2lplnj  30102  dalemzeo  30115  dath2  30219  lncvrat  30264  cdlemb  30276  elpaddri  30284  padd4N  30322  llnmod2i2  30345  llnexchb2  30351  dalawlem1  30353  dalawlem2  30354  osumcllem6N  30443  pexmidlem3N  30454  pexmidlem4N  30455  lhp2lt  30483  lhp2at0  30514  lhp2atne  30516  lhp2at0ne  30518  lhpmod2i2  30520  lhpmod6i1  30521  lhpat  30525  lhpat3  30528  4atexlemex6  30556  ltrncoval  30627  ltrncnv  30628  ltrnnidn  30656  cdlemd7  30686  cdleme0b  30694  cdleme0c  30695  cdleme0fN  30700  cdleme0ex1N  30705  cdleme7d  30728  cdleme7e  30729  cdleme7ga  30730  cdleme7  30731  cdleme11a  30742  cdleme17c  30770  cdleme22gb  30776  cdlemeda  30780  cdleme20k  30801  cdleme21a  30807  cdleme21at  30810  cdleme21d  30812  cdleme22f2  30829  cdleme22g  30830  cdleme24  30834  cdleme28  30855  cdlemefrs29cpre1  30880  cdlemefr29exN  30884  cdlemefr32sn2aw  30886  cdleme32fva  30919  cdleme32fva1  30920  cdleme35a  30930  cdleme42c  30954  cdleme42e  30961  cdleme42f  30962  cdleme42g  30963  cdleme42h  30964  cdleme43bN  30972  cdleme46f2g2  30975  cdleme17d2  30977  cdleme4gfv  30989  cdlemeg46c  30995  cdlemeg46nlpq  30999  cdlemeg46gfre  31014  cdlemeg49lebilem  31021  cdleme50trn1  31031  cdleme50trn2  31033  cdleme50ltrn  31039  cdleme  31042  cdlemf1  31043  cdlemf  31045  trlord  31051  ltrniotavalbN  31066  cdlemg1cex  31070  cdlemg2dN  31072  cdlemg2ce  31074  cdlemg2fvlem  31076  cdlemg2idN  31078  cdlemg2kq  31084  cdlemg2l  31085  cdlemg7fvN  31106  cdlemg7aN  31107  cdlemg8a  31109  cdlemg11aq  31120  cdlemg12d  31128  cdlemg13a  31133  cdlemg13  31134  cdlemg14f  31135  cdlemg14g  31136  cdlemg17b  31144  cdlemg27a  31174  cdlemg31b0N  31176  cdlemg31a  31179  cdlemg31b  31180  cdlemg31c  31181  ltrnco  31201  trlcoabs2N  31204  trlcocnvat  31206  trlconid  31207  trlcolem  31208  cdlemg42  31211  cdlemg43  31212  cdlemg47a  31216  cdlemg46  31217  cdlemg47  31218  tendoeq1  31246  tendocoval  31248  tendoco2  31250  tendoplco2  31261  tendopltp  31262  cdlemh1  31297  cdlemh2  31298  cdlemi1  31300  cdlemi  31302  cdlemk1  31313  cdlemk2  31314  cdlemk3  31315  cdlemk4  31316  cdlemk8  31320  cdlemk9  31321  cdlemk9bN  31322  cdlemk31  31378  cdlemk28-3  31390  cdlemk19xlem  31424  cdlemk39u  31450  cdlemk19u  31452  cdlemk56w  31455  cdlemn7  31686  cdlemn8  31687  cdlemn9  31688  dihordlem6  31696  dihordlem7  31697  dihordlem7b  31698  dihord1  31701  dihord2a  31702  dihord11c  31707  dihord2pre  31708  dihord2pre2  31709  dihlsscpre  31717  dihord4  31741  dihord6b  31743  dihmeetlem2N  31782  dihglbcpreN  31783  dihmeetcN  31785  dihmeetbclemN  31787  dihmeetlem3N  31788  dihmeetlem9N  31798  dihmeetlem13N  31802  dihmeetlem20N  31809  mapdpglem24  32187  mapdpglem32  32188  baerlem3lem2  32193  baerlem5alem2  32194  baerlem5blem2  32195  mapdh9aOLDN  32274  hdmap14lem6  32359
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-an 361  df-3an 938
  Copyright terms: Public domain W3C validator