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  5303  fsnunf  5720  f1oiso2  5851  omeulem2  6583  unxpdomlem3  7071  fin23lem11  7945  reclem3pr  8675  addid2  8997  dmdcan  9472  xaddass2  10572  xlt2add  10582  xadddi2  10619  expaddzlem  11147  expaddz  11148  expmulz  11150  expdiv  11154  ccatopth2  11465  o1add  12089  o1mul  12090  o1sub  12091  prmexpb  12798  pcpremul  12898  pcdiv  12907  pcqmul  12908  pcqdiv  12912  4sqlem12  13005  f1ocpbllem  13428  ercpbl  13453  erlecpbl  13454  latjlej12  14175  latmlem12  14191  latj4  14209  mndodcong  14859  cmn4  15110  ablsub4  15116  abladdsub4  15117  lsm4  15154  abvdom  15605  abvtrivd  15607  lspsnvs  15869  lspsneu  15878  lspfixed  15883  lspexch  15884  lsmcv  15896  lspsolvlem  15897  mvrf1  16172  coe1sclmulfv  16361  cnprest  17019  isreg2  17107  elptr  17270  hausflimlem  17676  ssbl  17973  prdsxmslem2  18077  tgqioo  18308  metnrm  18368  bndth  18458  cph2ass  18650  iscau3  18706  ovolunlem2  18859  dvres2  19264  dvfsumlem2  19376  dvfsum2  19383  deg1tm  19506  plyadd  19601  plymul  19602  coeeu  19609  coemullem  19633  aalioulem4  19717  cxplea  20045  cxple2  20046  cxplt2  20047  cxple2a  20048  cxpcn3lem  20089  angcan  20102  ang180lem5  20113  divsqrsumlem  20276  logexprlim  20466  dchrvmasumlema  20651  dchrisum0lema  20665  logdivsum  20684  log2sumbnd  20695  padicabv  20781  chscllem4  22221  mdslmd4i  22915  measxun  23541  mbfmco2  23572  dedekind  24084  brbtwn2  24535  axcontlem4  24597  axcontlem8  24601  cgrcomim  24614  cgrcoml  24621  cgrcomr  24622  cgrdegen  24629  btwnintr  24644  btwnexch3  24645  btwnouttr  24649  btwnexch  24650  btwndiff  24652  ifscgr  24669  lineid  24708  btwnconn1lem7  24718  btwnconn1lem8  24719  btwnconn1lem9  24720  btwnconn1lem12  24723  midofsegid  24729  brsegle2  24734  btwnoutside  24750  outsideoftr  24754  uninqs  25050  valcurfn2  25216  oriso  25225  islimrs  25591  islimrs3  25592  islimrs4  25593  icccon4  25713  isepic  25835  rocatval  25970  cnres2  26494  heibor  26556  mzpmfp  26836  mzpsubst  26837  pellexlem5  26929  pell14qrexpclnn0  26962  pellfundex  26982  qirropth  27004  monotuz  27037  expmordi  27043  congmul  27065  congsub  27068  mzpcong  27070  fzmaxdif  27079  jm2.15nn0  27107  symgsssg  27419  symgfisg  27420  idomsubgmo  27525  lsmsat  29271  lkrlsp  29365  lkrlsp2  29366  lkrlsp3  29367  lshpkrlem6  29378  latm4  29496  omlspjN  29524  hlatj4  29636  4noncolr3  29715  4noncolr2  29716  4noncolr1  29717  3dimlem3a  29722  3dimlem4a  29725  3dimlem4  29726  3dimlem4OLDN  29727  1cvratex  29735  hlatexch4  29743  3atlem4  29748  atcvrlln2  29781  atcvrlln  29782  llnmlplnN  29801  lplnnlelln  29805  lvoli2  29843  lvolnlelln  29846  lvolnlelpln  29847  4atlem11b  29870  4atlem12b  29873  2lplnj  29882  dalemzeo  29895  dath2  29999  lncvrat  30044  cdlemb  30056  elpaddri  30064  padd4N  30102  llnmod2i2  30125  llnexchb2  30131  dalawlem1  30133  dalawlem2  30134  osumcllem6N  30223  pexmidlem3N  30234  pexmidlem4N  30235  lhp2lt  30263  lhp2at0  30294  lhp2atne  30296  lhp2at0ne  30298  lhpmod2i2  30300  lhpmod6i1  30301  lhpat  30305  lhpat3  30308  4atexlemex6  30336  ltrncoval  30407  ltrncnv  30408  ltrnnidn  30436  cdlemd7  30466  cdleme0b  30474  cdleme0c  30475  cdleme0fN  30480  cdleme0ex1N  30485  cdleme7d  30508  cdleme7e  30509  cdleme7ga  30510  cdleme7  30511  cdleme11a  30522  cdleme17c  30550  cdleme22gb  30556  cdlemeda  30560  cdleme20k  30581  cdleme21a  30587  cdleme21at  30590  cdleme21d  30592  cdleme22f2  30609  cdleme22g  30610  cdleme24  30614  cdleme28  30635  cdlemefrs29cpre1  30660  cdlemefr29exN  30664  cdlemefr32sn2aw  30666  cdleme32fva  30699  cdleme32fva1  30700  cdleme35a  30710  cdleme42c  30734  cdleme42e  30741  cdleme42f  30742  cdleme42g  30743  cdleme42h  30744  cdleme43bN  30752  cdleme46f2g2  30755  cdleme17d2  30757  cdleme4gfv  30769  cdlemeg46c  30775  cdlemeg46nlpq  30779  cdlemeg46gfre  30794  cdlemeg49lebilem  30801  cdleme50trn1  30811  cdleme50trn2  30813  cdleme50ltrn  30819  cdleme  30822  cdlemf1  30823  cdlemf  30825  trlord  30831  ltrniotavalbN  30846  cdlemg1cex  30850  cdlemg2dN  30852  cdlemg2ce  30854  cdlemg2fvlem  30856  cdlemg2idN  30858  cdlemg2kq  30864  cdlemg2l  30865  cdlemg7fvN  30886  cdlemg7aN  30887  cdlemg8a  30889  cdlemg11aq  30900  cdlemg12d  30908  cdlemg13a  30913  cdlemg13  30914  cdlemg14f  30915  cdlemg14g  30916  cdlemg17b  30924  cdlemg27a  30954  cdlemg31b0N  30956  cdlemg31a  30959  cdlemg31b  30960  cdlemg31c  30961  ltrnco  30981  trlcoabs2N  30984  trlcocnvat  30986  trlconid  30987  trlcolem  30988  cdlemg42  30991  cdlemg43  30992  cdlemg47a  30996  cdlemg46  30997  cdlemg47  30998  tendoeq1  31026  tendocoval  31028  tendoco2  31030  tendoplco2  31041  tendopltp  31042  cdlemh1  31077  cdlemh2  31078  cdlemi1  31080  cdlemi  31082  cdlemk1  31093  cdlemk2  31094  cdlemk3  31095  cdlemk4  31096  cdlemk8  31100  cdlemk9  31101  cdlemk9bN  31102  cdlemk31  31158  cdlemk28-3  31170  cdlemk19xlem  31204  cdlemk39u  31230  cdlemk19u  31232  cdlemk56w  31235  cdlemn7  31466  cdlemn8  31467  cdlemn9  31468  dihordlem6  31476  dihordlem7  31477  dihordlem7b  31478  dihord1  31481  dihord2a  31482  dihord11c  31487  dihord2pre  31488  dihord2pre2  31489  dihlsscpre  31497  dihord4  31521  dihord6b  31523  dihmeetlem2N  31562  dihglbcpreN  31563  dihmeetcN  31565  dihmeetbclemN  31567  dihmeetlem3N  31568  dihmeetlem9N  31578  dihmeetlem13N  31582  dihmeetlem20N  31589  mapdpglem24  31967  mapdpglem32  31968  baerlem3lem2  31973  baerlem5alem2  31974  baerlem5blem2  31975  mapdh9aOLDN  32054  hdmap14lem6  32139
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