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

Theorem simp2r 982
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 447 . 2  |-  ( ( ps  /\  ch )  ->  ch )
213ad2ant2 977 1  |-  ( (
ph  /\  ( ps  /\ 
ch )  /\  th )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934
This theorem is referenced by:  simpl2r  1009  simpr2r  1015  simp12r  1069  simp22r  1075  simp32r  1081  funprg  5267  fsnunf  5680  f1oiso2  5811  omeulem2  6577  unxpdomlem3  7065  fin23lem11  7939  reclem3pr  8669  addid2  8991  dmdcan  9466  xaddass2  10566  xlt2add  10576  xadddi2  10613  expaddzlem  11141  expaddz  11142  expmulz  11144  expdiv  11148  ccatopth2  11459  o1add  12083  o1mul  12084  o1sub  12085  prmexpb  12792  pcpremul  12892  pcdiv  12901  pcqmul  12902  pcqdiv  12906  4sqlem12  12999  f1ocpbllem  13422  ercpbl  13447  erlecpbl  13448  latjlej12  14169  latmlem12  14185  latj4  14203  mndodcong  14853  cmn4  15104  ablsub4  15110  abladdsub4  15111  lsm4  15148  abvdom  15599  abvtrivd  15601  lspsnvs  15863  lspsneu  15872  lspfixed  15877  lspexch  15878  lsmcv  15890  lspsolvlem  15891  mvrf1  16166  coe1sclmulfv  16355  cnprest  17013  isreg2  17101  elptr  17264  hausflimlem  17670  ssbl  17967  prdsxmslem2  18071  tgqioo  18302  metnrm  18362  bndth  18452  cph2ass  18644  iscau3  18700  ovolunlem2  18853  dvres2  19258  dvfsumlem2  19370  dvfsum2  19377  deg1tm  19500  plyadd  19595  plymul  19596  coeeu  19603  coemullem  19627  aalioulem4  19711  cxplea  20039  cxple2  20040  cxplt2  20041  cxple2a  20042  cxpcn3lem  20083  angcan  20096  ang180lem5  20107  divsqrsumlem  20270  logexprlim  20460  dchrvmasumlema  20645  dchrisum0lema  20659  logdivsum  20678  log2sumbnd  20689  padicabv  20775  chscllem4  22215  mdslmd4i  22909  dedekind  23488  brbtwn2  23943  axcontlem4  24005  axcontlem8  24009  cgrcomim  24022  cgrcoml  24029  cgrcomr  24030  cgrdegen  24037  btwnintr  24052  btwnexch3  24053  btwnouttr  24057  btwnexch  24058  btwndiff  24060  ifscgr  24077  lineid  24116  btwnconn1lem7  24126  btwnconn1lem8  24127  btwnconn1lem9  24128  btwnconn1lem12  24131  midofsegid  24137  brsegle2  24142  btwnoutside  24158  outsideoftr  24162  uninqs  24449  valcurfn2  24616  oriso  24625  islimrs  24991  islimrs3  24992  islimrs4  24993  icccon4  25113  isepic  25235  rocatval  25370  cnres2  25894  heibor  25956  mzpmfp  26236  mzpsubst  26237  pellexlem5  26329  pell14qrexpclnn0  26362  pellfundex  26382  qirropth  26404  monotuz  26437  expmordi  26443  congmul  26465  congsub  26468  mzpcong  26470  fzmaxdif  26479  jm2.15nn0  26507  symgsssg  26819  symgfisg  26820  idomsubgmo  26925  lsmsat  28477  lkrlsp  28571  lkrlsp2  28572  lkrlsp3  28573  lshpkrlem6  28584  latm4  28702  omlspjN  28730  hlatj4  28842  4noncolr3  28921  4noncolr2  28922  4noncolr1  28923  3dimlem3a  28928  3dimlem4a  28931  3dimlem4  28932  3dimlem4OLDN  28933  1cvratex  28941  hlatexch4  28949  3atlem4  28954  atcvrlln2  28987  atcvrlln  28988  llnmlplnN  29007  lplnnlelln  29011  lvoli2  29049  lvolnlelln  29052  lvolnlelpln  29053  4atlem11b  29076  4atlem12b  29079  2lplnj  29088  dalemzeo  29101  dath2  29205  lncvrat  29250  cdlemb  29262  elpaddri  29270  padd4N  29308  llnmod2i2  29331  llnexchb2  29337  dalawlem1  29339  dalawlem2  29340  osumcllem6N  29429  pexmidlem3N  29440  pexmidlem4N  29441  lhp2lt  29469  lhp2at0  29500  lhp2atne  29502  lhp2at0ne  29504  lhpmod2i2  29506  lhpmod6i1  29507  lhpat  29511  lhpat3  29514  4atexlemex6  29542  ltrncoval  29613  ltrncnv  29614  ltrnnidn  29642  cdlemd7  29672  cdleme0b  29680  cdleme0c  29681  cdleme0fN  29686  cdleme0ex1N  29691  cdleme7d  29714  cdleme7e  29715  cdleme7ga  29716  cdleme7  29717  cdleme11a  29728  cdleme17c  29756  cdleme22gb  29762  cdlemeda  29766  cdleme20k  29787  cdleme21a  29793  cdleme21at  29796  cdleme21d  29798  cdleme22f2  29815  cdleme22g  29816  cdleme24  29820  cdleme28  29841  cdlemefrs29cpre1  29866  cdlemefr29exN  29870  cdlemefr32sn2aw  29872  cdleme32fva  29905  cdleme32fva1  29906  cdleme35a  29916  cdleme42c  29940  cdleme42e  29947  cdleme42f  29948  cdleme42g  29949  cdleme42h  29950  cdleme43bN  29958  cdleme46f2g2  29961  cdleme17d2  29963  cdleme4gfv  29975  cdlemeg46c  29981  cdlemeg46nlpq  29985  cdlemeg46gfre  30000  cdlemeg49lebilem  30007  cdleme50trn1  30017  cdleme50trn2  30019  cdleme50ltrn  30025  cdleme  30028  cdlemf1  30029  cdlemf  30031  trlord  30037  ltrniotavalbN  30052  cdlemg1cex  30056  cdlemg2dN  30058  cdlemg2ce  30060  cdlemg2fvlem  30062  cdlemg2idN  30064  cdlemg2kq  30070  cdlemg2l  30071  cdlemg7fvN  30092  cdlemg7aN  30093  cdlemg8a  30095  cdlemg11aq  30106  cdlemg12d  30114  cdlemg13a  30119  cdlemg13  30120  cdlemg14f  30121  cdlemg14g  30122  cdlemg17b  30130  cdlemg27a  30160  cdlemg31b0N  30162  cdlemg31a  30165  cdlemg31b  30166  cdlemg31c  30167  ltrnco  30187  trlcoabs2N  30190  trlcocnvat  30192  trlconid  30193  trlcolem  30194  cdlemg42  30197  cdlemg43  30198  cdlemg47a  30202  cdlemg46  30203  cdlemg47  30204  tendoeq1  30232  tendocoval  30234  tendoco2  30236  tendoplco2  30247  tendopltp  30248  cdlemh1  30283  cdlemh2  30284  cdlemi1  30286  cdlemi  30288  cdlemk1  30299  cdlemk2  30300  cdlemk3  30301  cdlemk4  30302  cdlemk8  30306  cdlemk9  30307  cdlemk9bN  30308  cdlemk31  30364  cdlemk28-3  30376  cdlemk19xlem  30410  cdlemk39u  30436  cdlemk19u  30438  cdlemk56w  30441  cdlemn7  30672  cdlemn8  30673  cdlemn9  30674  dihordlem6  30682  dihordlem7  30683  dihordlem7b  30684  dihord1  30687  dihord2a  30688  dihord11c  30693  dihord2pre  30694  dihord2pre2  30695  dihlsscpre  30703  dihord4  30727  dihord6b  30729  dihmeetlem2N  30768  dihglbcpreN  30769  dihmeetcN  30771  dihmeetbclemN  30773  dihmeetlem3N  30774  dihmeetlem9N  30784  dihmeetlem13N  30788  dihmeetlem20N  30795  mapdpglem24  31173  mapdpglem32  31174  baerlem3lem2  31179  baerlem5alem2  31180  baerlem5blem2  31181  mapdh9aOLDN  31260  hdmap14lem6  31345
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 177  df-an 360  df-3an 936
  Copyright terms: Public domain W3C validator