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

Theorem simpr2 1012
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 1006 . 2  |-  ( ( ps  /\  ch  /\  th )  ->  ch )
21adantl 467 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:  simplr2  1048  simprr2  1054  simp1r2  1102  simp2r2  1108  simp3r2  1114  3anandis  1366  wereu  4850  fpr2g  6140  isopolem  6251  fr3nr  6620  frfi  7822  intrnfi  7936  fisupcl  7991  cnfcomlem  8203  ackbij1lem15  8662  cofsmo  8697  sornom  8705  fpwwe2lem5  9058  dedekindle  9797  supmul1  10576  eluzuzle  11167  xlesubadd  11549  elioc2  11697  elico2  11698  elicc2  11699  fseq1p1m1  11866  fz0fzelfz0  11894  swrdsbslen  12789  swrdspsleq  12790  ccatswrd  12797  swrdswrdlem  12800  tanadd  14199  dvds2ln  14311  cshwsidrepsw  15027  ressress  15149  f1ovscpbl  15383  mreexexlem4d  15504  mreexexd  15505  iscatd2  15538  2oppccomf  15581  issubc3  15705  fthmon  15783  fuccocl  15820  fucidcl  15821  invfuc  15830  initoeu2lem0  15859  initoeu2lem1  15860  curf2cl  16067  yonedalem4c  16113  yonedalem3  16116  pospo  16170  latjle12  16259  latjlej1  16262  latnlej2  16268  latlem12  16275  latmlem1  16278  latledi  16286  latjass  16292  latj12  16293  latj32  16294  latj13  16295  latj31  16296  latjrot  16297  latjjdi  16300  latjjdir  16301  latdisdlem  16386  prdsmndd  16520  frmdmnd  16594  grpsubrcan  16686  grpsubadd  16693  grpaddsubass  16695  grpsubsub4  16698  grppnpcan2  16699  grpnpncan  16700  mulgnndir  16731  mulgnn0dir  16732  mulgdir  16734  mulgnnass  16737  mulgnn0ass  16738  mulgass  16739  mulgsubdir  16740  pwsmulg  16751  issubg2  16783  eqgval  16817  qusgrp  16823  galcan  16909  gacan  16910  oppgmnd  16956  symggrp  16992  fvcosymgeq  17021  pmtrprfv  17045  psgnunilem3  17088  cmn32  17383  cmn12  17385  abladdsub  17392  mulgdi  17402  mulgsubdi  17405  dprdss  17597  dprdz  17598  dprdf1o  17600  dprdsn  17604  dprd2da  17610  dmdprdsplit  17615  ablfac1b  17638  pgpfac1lem5  17647  srgi  17680  srgbinom  17713  ringi  17728  prdsringd  17775  opprring  17794  mulgass3  17800  dvrass  17853  subrgunit  17961  issubrg2  17963  abvdiv  18000  lsssn0  18106  islss3  18117  prdslmodd  18127  islmhm2  18196  lspsolv  18301  islbs2  18312  islbs3  18313  lbsextlem4  18319  sralmod  18345  issubassa  18483  sraassa  18484  psrbaglesupp  18527  psrbaglecl  18528  psrbagcon  18530  psrgrp  18557  psrlmod  18560  psrring  18570  psrassa  18573  psgndiflemB  19099  ipdir  19137  ipdi  19138  ipsubdir  19140  ipsubdi  19141  ipass  19143  ipassr  19144  ipassr2  19145  isphld  19152  ocvlss  19166  mamudm  19344  matring  19399  matassa  19400  ofco2  19407  ma1repveval  19527  mdetunilem1  19568  mdetunilem9  19576  chpscmatgsumbin  19799  iinopn  19863  restopnb  20122  subbascn  20201  nrmsep2  20303  isnrm3  20306  regsep2  20323  dnsconst  20325  dfcon2  20365  1stcelcls  20407  dislly  20443  ptuni2  20522  tx1stc  20596  0nelfb  20777  infil  20809  fsubbas  20813  filssufilg  20857  hauspwpwf1  20933  cnextcn  21013  tmdcn2  21035  ustuqtoplem  21185  utopsnneiplem  21193  psmettri  21258  isxmet2d  21273  xmettri  21297  xmetres2  21307  bldisj  21344  blss2ps  21349  blss2  21350  xmstri2  21412  mstri2  21413  xmstri  21414  mstri  21415  xmstri3  21416  mstri3  21417  msrtri  21418  comet  21459  stdbdbl  21463  met2ndci  21468  ngprcan  21554  ngplcan  21555  ngpsubcan  21558  nrgdsdi  21599  nrgdsdir  21600  nlmdsdi  21615  nlmdsdir  21616  blcvx  21727  icoopnst  21863  pi1grplem  21973  cvsdiv  22033  cvsdivcl  22034  cphdivcl  22053  cphsubdir  22078  cphsubdi  22079  tchcph  22104  bcthlem5  22189  volfiniun  22377  volcn  22441  itg1val2  22519  dvconst  22748  dvlip  22822  ftc1a  22866  ulmval  23200  ulmdvlem3  23222  ang180  23608  cvxcl  23775  scvxcvx  23776  sgmmul  23992  dchrabl  24045  motgrp  24448  iscgra1  24708  cgrane1  24710  cgrane3  24712  cgrahl1  24714  cgrahl2  24715  cgracgr  24716  cgratr  24721  cgrabtwn  24722  cgrahl  24723  dfcgra2  24726  f1otrge  24748  colinearalglem1  24782  axcgrtr  24791  axeuclidlem  24838  axcontlem3  24842  axcontlem4  24843  axcontlem7  24846  eengtrkg  24861  eengtrkge  24862  isspthonpth  25159  wlkdvspth  25183  clwlkfoclwwlk  25418  el2spthonot0  25444  el2wlkonotot0  25445  usg2wotspth  25457  2spontn0vne  25460  rusgranumwlks  25529  rusgranumwwlkg  25532  iseupa  25538  3vfriswmgra  25578  frgrareggt1  25689  grpomuldivass  25822  grponpncan  25828  grpodiveq  25829  ablomuldiv  25862  ablodivdiv4  25864  ablonnncan1  25868  nvmdi  26116  nvsubadd  26121  dipassr  26332  archiabllem2c  28350  dvrdir  28392  dvrcan5  28395  reofld  28442  pstmfval  28538  qqhval2lem  28624  qqhvq  28630  measdivcstOLD  28885  measdivcst  28886  carsggect  28979  bnj1098  29383  bnj149  29474  bnj1118  29581  erdszelem9  29710  rescon  29757  cvmseu  29787  cvmlift2lem10  29823  cvmlift2lem12  29825  elmrsubrn  29946  mclsind  29996  frrlem4  30304  cgrid2  30555  segconeu  30563  btwncomim  30565  btwnswapid  30569  trisegint  30580  cgrxfr  30607  brofs2  30629  endofsegid  30637  btwnconn2  30654  seglemin  30665  segletr  30666  btwnsegle  30669  colinbtwnle  30670  broutsideof2  30674  btwnoutside  30677  broutsideof3  30678  outsideoftr  30681  outsidele  30684  fvray  30693  fvline  30696  ellines  30704  broucube  31677  ftc1anc  31728  sdclem1  31775  sstotbnd2  31809  iscringd  31935  lsmsat  32282  lfladdcl  32345  lflnegcl  32349  lflvscl  32351  eqlkr  32373  lshpkrlem4  32387  lshpkrlem6  32389  ldualgrplem  32419  lduallmodlem  32426  latmassOLD  32503  latm12  32504  latm32  32505  latmrot  32506  latmmdiN  32508  latmmdir  32509  omlfh1N  32532  omlfh3N  32533  cvrnbtwn2  32549  cvlexchb1  32604  cvlsupr2  32617  hlatjass  32643  hlatj12  32644  hlatj32  32645  cvrat  32695  cvrat2  32702  atltcvr  32708  atexchltN  32714  cvrat3  32715  cvrat4  32716  atbtwnexOLDN  32720  atbtwnex  32721  3dimlem3  32734  3dimlem3OLDN  32735  3at  32763  2atneat  32788  llncmp  32795  2at0mat0  32798  2atmat0  32799  llncvrlpln  32831  lplncmp  32835  2llnjaN  32839  4atlem11  32882  lplncvrlvol  32889  lvolcmp  32890  2atm2atN  33058  elpaddatriN  33076  paddasslem8  33100  paddass  33111  padd12N  33112  paddssw2  33117  paddss  33118  pmod1i  33121  pmodN  33123  pmapjlln1  33128  atmod1i1  33130  atmod1i2  33132  pexmidlem2N  33244  pl42lem2N  33253  pl42lem3N  33254  pl42lem4N  33255  pl42N  33256  lhpm0atN  33302  lautlt  33364  lautcvr  33365  lautj  33366  lautm  33367  ltrneq2  33421  cdlemd1  33472  cdleme1b  33500  cdleme1  33501  cdleme2  33502  cdleme3e  33506  cdlemefr27cl  33678  cdlemefs27cl  33688  cdleme42ke  33760  cdleme42mN  33762  cdlemf2  33837  cdlemftr2  33841  trljco  34015  tgrpgrplem  34024  tendoplass  34058  tendodi1  34059  tendodi2  34060  cdlemk34  34185  cdlemk36  34188  erngdvlem3-rN  34273  tendospdi1  34296  dialss  34322  dvhvaddass  34373  dvhopvsca  34378  dvhlveclem  34384  diblss  34446  diclss  34469  diclspsn  34470  cdlemn11pre  34486  dihmeetlem12N  34594  dihmeetlem16N  34598  dihmeetlem17N  34599  dihmeetlem18N  34600  dvh4dimN  34723  lpolconN  34763  dochpolN  34766  lclkr  34809  lclkrs  34815  lcfr  34861  irrapxlem6  35380  jm2.26lem3  35561  dgrsub2  35699  mpaaroot  35719  mendring  35756  mendlmod  35757  mendassa  35758  relexpmulg  35940  iunrelexpmin2  35942  relexpxpmin  35947  rfcnpre3  36993  fmuldfeq  37232  stoweidlem43  37472  stoweidlem52  37481  stoweidlem53  37482  stoweidlem56  37485  stoweidlem57  37486  stoweidlem60  37489  iccpartigtl  38126  iccelpart  38136  ltsubsubaddltsub  38396  copissgrp  38565  cznrng  38714  funcringcsetcALTV2lem9  38803  funcringcsetclem9ALTV  38826  ldepsprlem  39024  lincresunit3  39033  lincreslvec3  39034
  Copyright terms: Public domain W3C validator