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

Theorem simpr2 1021
Description: Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.)
Assertion
Ref Expression
simpr2  |-  ( (
ph  /\  ( ps  /\ 
ch  /\  th )
)  ->  ch )

Proof of Theorem simpr2
StepHypRef Expression
1 simp2 1015 . 2  |-  ( ( ps  /\  ch  /\  th )  ->  ch )
21adantl 472 1  |-  ( (
ph  /\  ( ps  /\ 
ch  /\  th )
)  ->  ch )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 375    /\ w3a 991
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 190  df-an 377  df-3an 993
This theorem is referenced by:  simplr2  1057  simprr2  1063  simp1r2  1111  simp2r2  1117  simp3r2  1123  3anandis  1381  wereu  4852  fpr2g  6155  isopolem  6266  fr3nr  6638  frfi  7847  intrnfi  7961  fisupcl  8016  cnfcomlem  8235  ackbij1lem15  8695  cofsmo  8730  sornom  8738  fpwwe2lem5  9090  dedekindle  9829  supmul1  10609  eluzuzle  11201  xlesubadd  11583  elioc2  11731  elico2  11732  elicc2  11733  fseq1p1m1  11903  fz0fzelfz0  11932  swrdsbslen  12847  swrdspsleq  12848  ccatswrd  12855  swrdswrdlem  12858  tanadd  14276  dvds2ln  14388  cshwsidrepsw  15119  ressress  15242  f1ovscpbl  15487  mreexexlem4d  15608  mreexexd  15609  iscatd2  15642  2oppccomf  15685  issubc3  15809  fthmon  15887  fuccocl  15924  fucidcl  15925  invfuc  15934  initoeu2lem0  15963  initoeu2lem1  15964  curf2cl  16171  yonedalem4c  16217  yonedalem3  16220  pospo  16274  latjle12  16363  latjlej1  16366  latnlej2  16372  latlem12  16379  latmlem1  16382  latledi  16390  latjass  16396  latj12  16397  latj32  16398  latj13  16399  latj31  16400  latjrot  16401  latjjdi  16404  latjjdir  16405  latdisdlem  16490  prdsmndd  16624  frmdmnd  16698  grpsubrcan  16790  grpsubadd  16797  grpaddsubass  16799  grpsubsub4  16802  grppnpcan2  16803  grpnpncan  16804  mulgnndir  16835  mulgnn0dir  16836  mulgdir  16838  mulgnnass  16841  mulgnn0ass  16842  mulgass  16843  mulgsubdir  16844  pwsmulg  16855  issubg2  16887  eqgval  16921  qusgrp  16927  galcan  17013  gacan  17014  oppgmnd  17060  symggrp  17096  fvcosymgeq  17125  pmtrprfv  17149  psgnunilem3  17192  cmn32  17503  cmn12  17505  abladdsub  17512  mulgdi  17522  mulgsubdi  17525  dprdss  17717  dprdz  17718  dprdf1o  17720  dprdsn  17724  dprd2da  17730  dmdprdsplit  17735  ablfac1b  17758  pgpfac1lem5  17767  srgi  17800  srgbinom  17833  ringi  17848  prdsringd  17895  opprring  17914  mulgass3  17920  dvrass  17973  subrgunit  18081  issubrg2  18083  abvdiv  18120  lsssn0  18226  islss3  18237  prdslmodd  18247  islmhm2  18316  lspsolv  18421  islbs2  18432  islbs3  18433  lbsextlem4  18439  sralmod  18465  issubassa  18603  sraassa  18604  psrbaglesupp  18647  psrbaglecl  18648  psrbagcon  18650  psrgrp  18677  psrlmod  18680  psrring  18690  psrassa  18693  psgndiflemB  19223  ipdir  19261  ipdi  19262  ipsubdir  19264  ipsubdi  19265  ipass  19267  ipassr  19268  ipassr2  19269  isphld  19276  ocvlss  19290  mamudm  19468  matring  19523  matassa  19524  ofco2  19531  ma1repveval  19651  mdetunilem1  19692  mdetunilem9  19700  chpscmatgsumbin  19923  iinopn  19987  restopnb  20246  subbascn  20325  nrmsep2  20427  isnrm3  20430  regsep2  20447  dnsconst  20449  dfcon2  20489  1stcelcls  20531  dislly  20567  ptuni2  20646  tx1stc  20720  0nelfb  20901  infil  20933  fsubbas  20937  filssufilg  20981  hauspwpwf1  21057  cnextcn  21137  tmdcn2  21159  ustuqtoplem  21309  utopsnneiplem  21317  psmettri  21382  isxmet2d  21397  xmettri  21421  xmetres2  21431  bldisj  21468  blss2ps  21473  blss2  21474  xmstri2  21536  mstri2  21537  xmstri  21538  mstri  21539  xmstri3  21540  mstri3  21541  msrtri  21542  comet  21583  stdbdbl  21587  met2ndci  21592  ngprcan  21678  ngplcan  21679  ngpsubcan  21682  nrgdsdi  21723  nrgdsdir  21724  nlmdsdi  21739  nlmdsdir  21740  blcvx  21871  icoopnst  22022  pi1grplem  22135  cvsdiv  22195  cvsdivcl  22196  cphdivcl  22215  cphsubdir  22240  cphsubdi  22241  tchcph  22266  bcthlem5  22351  volfiniun  22556  volcn  22620  itg1val2  22698  dvconst  22927  dvlip  23001  ftc1a  23045  ulmval  23391  ulmdvlem3  23413  ang180  23799  cvxcl  23966  scvxcvx  23967  sgmmul  24185  dchrabl  24238  motgrp  24644  iscgra1  24908  cgrane1  24910  cgrane3  24912  cgrahl1  24914  cgrahl2  24915  cgracgr  24916  cgratr  24921  cgrabtwn  24923  cgrahl  24924  dfcgra2  24927  sacgr  24928  f1otrge  24958  colinearalglem1  24992  axcgrtr  25001  axeuclidlem  25048  axcontlem3  25052  axcontlem4  25053  axcontlem7  25056  eengtrkg  25071  eengtrkge  25072  isspthonpth  25370  wlkdvspth  25394  clwlkfoclwwlk  25629  el2spthonot0  25655  el2wlkonotot0  25656  usg2wotspth  25668  2spontn0vne  25671  rusgranumwlks  25740  rusgranumwwlkg  25743  iseupa  25749  3vfriswmgra  25789  frgrareggt1  25900  grpomuldivass  26033  grponpncan  26039  grpodiveq  26040  ablomuldiv  26073  ablodivdiv4  26075  ablonnncan1  26079  nvmdi  26327  nvsubadd  26332  dipassr  26543  archiabllem2c  28563  dvrdir  28604  dvrcan5  28607  reofld  28654  pstmfval  28750  qqhval2lem  28836  qqhvq  28842  measdivcstOLD  29097  measdivcst  29098  carsggect  29200  bnj1098  29645  bnj149  29736  bnj1118  29843  erdszelem9  29972  rescon  30019  cvmseu  30049  cvmlift2lem10  30085  cvmlift2lem12  30087  elmrsubrn  30208  mclsind  30258  frrlem4  30567  cgrid2  30820  segconeu  30828  btwncomim  30830  btwnswapid  30834  trisegint  30845  cgrxfr  30872  brofs2  30894  endofsegid  30902  btwnconn2  30919  seglemin  30930  segletr  30931  btwnsegle  30934  colinbtwnle  30935  broutsideof2  30939  btwnoutside  30942  broutsideof3  30943  outsideoftr  30946  outsidele  30949  fvray  30958  fvline  30961  ellines  30969  broucube  32020  ftc1anc  32071  sdclem1  32118  sstotbnd2  32152  iscringd  32278  lsmsat  32620  lfladdcl  32683  lflnegcl  32687  lflvscl  32689  eqlkr  32711  lshpkrlem4  32725  lshpkrlem6  32727  ldualgrplem  32757  lduallmodlem  32764  latmassOLD  32841  latm12  32842  latm32  32843  latmrot  32844  latmmdiN  32846  latmmdir  32847  omlfh1N  32870  omlfh3N  32871  cvrnbtwn2  32887  cvlexchb1  32942  cvlsupr2  32955  hlatjass  32981  hlatj12  32982  hlatj32  32983  cvrat  33033  cvrat2  33040  atltcvr  33046  atexchltN  33052  cvrat3  33053  cvrat4  33054  atbtwnexOLDN  33058  atbtwnex  33059  3dimlem3  33072  3dimlem3OLDN  33073  3at  33101  2atneat  33126  llncmp  33133  2at0mat0  33136  2atmat0  33137  llncvrlpln  33169  lplncmp  33173  2llnjaN  33177  4atlem11  33220  lplncvrlvol  33227  lvolcmp  33228  2atm2atN  33396  elpaddatriN  33414  paddasslem8  33438  paddass  33449  padd12N  33450  paddssw2  33455  paddss  33456  pmod1i  33459  pmodN  33461  pmapjlln1  33466  atmod1i1  33468  atmod1i2  33470  pexmidlem2N  33582  pl42lem2N  33591  pl42lem3N  33592  pl42lem4N  33593  pl42N  33594  lhpm0atN  33640  lautlt  33702  lautcvr  33703  lautj  33704  lautm  33705  ltrneq2  33759  cdlemd1  33810  cdleme1b  33838  cdleme1  33839  cdleme2  33840  cdleme3e  33844  cdlemefr27cl  34016  cdlemefs27cl  34026  cdleme42ke  34098  cdleme42mN  34100  cdlemf2  34175  cdlemftr2  34179  trljco  34353  tgrpgrplem  34362  tendoplass  34396  tendodi1  34397  tendodi2  34398  cdlemk34  34523  cdlemk36  34526  erngdvlem3-rN  34611  tendospdi1  34634  dialss  34660  dvhvaddass  34711  dvhopvsca  34716  dvhlveclem  34722  diblss  34784  diclss  34807  diclspsn  34808  cdlemn11pre  34824  dihmeetlem12N  34932  dihmeetlem16N  34936  dihmeetlem17N  34937  dihmeetlem18N  34938  dvh4dimN  35061  lpolconN  35101  dochpolN  35104  lclkr  35147  lclkrs  35153  lcfr  35199  irrapxlem6  35717  jm2.26lem3  35902  dgrsub2  36040  mpaaroot  36067  mendring  36104  mendlmod  36105  mendassa  36106  relexpmulg  36348  iunrelexpmin2  36350  relexpxpmin  36355  rfcnpre3  37395  fmuldfeq  37747  stoweidlem43  38005  stoweidlem52  38014  stoweidlem53  38015  stoweidlem56  38018  stoweidlem57  38019  stoweidlem60  38022  iccpartigtl  38872  iccelpart  38882  ltsubsubaddltsub  39186  subgruhgredgd  39502  nbfusgrlevtxm2  39598  upgr1wlkwlk  39796  lfgriswlk  39819  3spthd  40013  copissgrp  40177  cznrng  40326  funcringcsetcALTV2lem9  40415  funcringcsetclem9ALTV  40438  ldepsprlem  40634  lincresunit3  40643  lincreslvec3  40644
  Copyright terms: Public domain W3C validator