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

Theorem simpr2 1003
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 997 . 2  |-  ( ( ps  /\  ch  /\  th )  ->  ch )
21adantl 466 1  |-  ( (
ph  /\  ( ps  /\ 
ch  /\  th )
)  ->  ch )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 973
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 185  df-an 371  df-3an 975
This theorem is referenced by:  simplr2  1039  simprr2  1045  simp1r2  1093  simp2r2  1099  simp3r2  1105  3anandis  1330  wereu  4875  isopolem  6227  fr3nr  6593  frfi  7761  intrnfi  7872  fisupcl  7923  cnfcomlem  8139  cnfcomlemOLD  8147  ackbij1lem15  8610  cofsmo  8645  sornom  8653  fpwwe2lem5  9008  dedekindle  9740  supmul1  10504  eluzuzle  11086  xlesubadd  11451  elioc2  11583  elico2  11584  elicc2  11585  fseq1p1m1  11748  fz0fzelfz0  11774  swrdsymbeq  12631  ccatswrd  12640  swrdswrdlem  12643  tanadd  13759  dvds2ln  13871  cshwsidrepsw  14432  ressress  14548  f1ovscpbl  14777  mreexexlem4d  14898  mreexexd  14899  iscatd2  14932  2oppccomf  14977  issubc3  15072  fthmon  15150  fuccocl  15187  fucidcl  15188  invfuc  15197  curf2cl  15354  yonedalem4c  15400  yonedalem3  15403  pospo  15456  latjle12  15545  latjlej1  15548  latnlej2  15554  latlem12  15561  latmlem1  15564  latledi  15572  latjass  15578  latj12  15579  latj32  15580  latj13  15581  latj31  15582  latjrot  15583  latjjdi  15586  latjjdir  15587  latdisdlem  15672  prdsmndd  15767  frmdmnd  15850  grpsubrcan  15920  grpsubadd  15927  grpaddsubass  15929  grpsubsub4  15932  grppnpcan2  15933  grpnpncan  15934  mulgnndir  15964  mulgnn0dir  15965  mulgdir  15967  mulgnnass  15970  mulgnn0ass  15971  mulgass  15972  mulgsubdir  15973  pwsmulg  15984  issubg2  16011  eqgval  16045  divsgrp  16051  galcan  16137  gacan  16138  oppgmnd  16184  symggrp  16220  fvcosymgeq  16249  pmtrprfv  16274  psgnunilem3  16317  cmn32  16612  cmn12  16614  abladdsub  16621  mulgdi  16631  mulgsubdi  16634  dprdss  16866  dprdz  16867  dprdf1o  16869  dprdsn  16873  dprd2da  16881  dmdprdsplit  16886  ablfac1b  16911  pgpfac1lem5  16920  srgi  16953  srgbinom  16984  rngi  16998  prdsrngd  17045  opprrng  17064  mulgass3  17070  dvrass  17123  subrgunit  17230  issubrg2  17232  abvdiv  17269  lsssn0  17377  islss3  17388  prdslmodd  17398  islmhm2  17467  lspsolv  17572  islbs2  17583  islbs3  17584  lbsextlem4  17590  sralmod  17616  issubassa  17744  sraassa  17745  psrbaglesupp  17788  psrbaglesuppOLD  17789  psrbaglecl  17790  psrbagcon  17793  psrgrp  17822  psrlmod  17825  psrrng  17837  psrassa  17840  psgndiflemB  18403  ipdir  18441  ipdi  18442  ipsubdir  18444  ipsubdi  18445  ipass  18447  ipassr  18448  ipassr2  18449  isphld  18456  ocvlss  18470  mamudm  18657  matrng  18712  matassa  18713  ofco2  18720  ma1repveval  18840  mdetunilem1  18881  mdetunilem9  18889  chpscmatgsumbin  19112  iinopn  19178  restopnb  19442  subbascn  19521  nrmsep2  19623  isnrm3  19626  regsep2  19643  dnsconst  19645  dfcon2  19686  1stcelcls  19728  dislly  19764  ptuni2  19812  tx1stc  19886  0nelfb  20067  infil  20099  fsubbas  20103  filssufilg  20147  hauspwpwf1  20223  cnextcn  20302  tmdcn2  20323  ustuqtoplem  20477  utopsnneiplem  20485  psmettri  20550  isxmet2d  20565  xmettri  20589  xmetres2  20599  bldisj  20636  blss2ps  20641  blss2  20642  xmstri2  20704  mstri2  20705  xmstri  20706  mstri  20707  xmstri3  20708  mstri3  20709  msrtri  20710  comet  20751  stdbdbl  20755  met2ndci  20760  ngprcan  20864  ngplcan  20865  ngpsubcan  20868  nrgdsdi  20909  nrgdsdir  20910  nlmdsdi  20925  nlmdsdir  20926  blcvx  21038  icoopnst  21174  pi1grplem  21284  cvsdiv  21344  cvsdivcl  21345  cphdivcl  21364  cphsubdir  21389  cphsubdi  21390  tchcph  21415  bcthlem5  21502  volfiniun  21692  volcn  21750  itg1val2  21826  dvconst  22055  dvlip  22129  ftc1a  22173  ulmval  22509  ulmdvlem3  22531  ang180  22874  cvxcl  23042  scvxcvx  23043  sgmmul  23204  dchrabl  23257  motgrp  23658  f1otrge  23851  xmstrkgc  23865  colinearalglem1  23885  axcgrtr  23894  axeuclidlem  23941  axcontlem3  23945  axcontlem4  23946  axcontlem7  23949  eengtrkg  23964  eengtrkge  23965  isspthonpth  24262  wlkdvspth  24286  clwlkfoclwwlk  24521  el2spthonot0  24547  usg2wotspth  24560  2spontn0vne  24563  rusgranumwlks  24632  rusgranumwwlkg  24635  iseupa  24641  3vfriswmgra  24681  frgrareggt1  24793  grpomuldivass  24927  grponpncan  24933  grpodiveq  24934  ablomuldiv  24967  ablodivdiv4  24969  ablonnncan1  24973  nvmdi  25221  nvsubadd  25226  dipassr  25437  archiabllem2c  27401  dvrdir  27443  dvrcan5  27446  reofld  27493  pstmfval  27511  qqhval2lem  27598  qqhvq  27604  measdivcstOLD  27835  measdivcst  27836  erdszelem9  28283  rescon  28331  cvmseu  28361  cvmlift2lem10  28397  cvmlift2lem12  28399  frrlem4  28967  cgrid2  29230  segconeu  29238  btwncomim  29240  btwnswapid  29244  trisegint  29255  cgrxfr  29282  brofs2  29304  endofsegid  29312  btwnconn2  29329  seglemin  29340  segletr  29341  btwnsegle  29344  colinbtwnle  29345  broutsideof2  29349  btwnoutside  29352  broutsideof3  29353  outsideoftr  29356  outsidele  29359  fvray  29368  fvline  29371  ellines  29379  ftc1anc  29675  sdclem1  29839  sstotbnd2  29873  iscringd  29999  irrapxlem6  30367  jm2.26lem3  30547  dgrsub2  30688  mpaaroot  30709  mendrng  30746  mendlmod  30747  mendassa  30748  rfcnpre3  30986  fmuldfeq  31133  stoweidlem43  31343  stoweidlem52  31352  stoweidlem53  31353  stoweidlem56  31356  stoweidlem57  31357  stoweidlem60  31360  ltsubsubaddltsub  31793  ldepsprlem  32146  lincresunit3  32155  lincreslvec3  32156  bnj1098  32921  bnj149  33012  bnj1118  33119  lsmsat  33805  lfladdcl  33868  lflnegcl  33872  lflvscl  33874  eqlkr  33896  lshpkrlem4  33910  lshpkrlem6  33912  ldualgrplem  33942  lduallmodlem  33949  latmassOLD  34026  latm12  34027  latm32  34028  latmrot  34029  latmmdiN  34031  latmmdir  34032  omlfh1N  34055  omlfh3N  34056  cvrnbtwn2  34072  cvlexchb1  34127  cvlsupr2  34140  hlatjass  34166  hlatj12  34167  hlatj32  34168  cvrat  34218  cvrat2  34225  atltcvr  34231  atexchltN  34237  cvrat3  34238  cvrat4  34239  atbtwnexOLDN  34243  atbtwnex  34244  3dimlem3  34257  3dimlem3OLDN  34258  3at  34286  2atneat  34311  llncmp  34318  2at0mat0  34321  2atmat0  34322  llncvrlpln  34354  lplncmp  34358  2llnjaN  34362  4atlem11  34405  lplncvrlvol  34412  lvolcmp  34413  2atm2atN  34581  elpaddatriN  34599  paddasslem8  34623  paddass  34634  padd12N  34635  paddssw2  34640  paddss  34641  pmod1i  34644  pmodN  34646  pmapjlln1  34651  atmod1i1  34653  atmod1i2  34655  pexmidlem2N  34767  pl42lem2N  34776  pl42lem3N  34777  pl42lem4N  34778  pl42N  34779  lhpm0atN  34825  lautlt  34887  lautcvr  34888  lautj  34889  lautm  34890  ltrneq2  34944  cdlemd1  34994  cdleme1b  35022  cdleme1  35023  cdleme2  35024  cdleme3e  35028  cdlemefr27cl  35199  cdlemefs27cl  35209  cdleme42ke  35281  cdleme42mN  35283  cdlemf2  35358  cdlemftr2  35362  trljco  35536  tgrpgrplem  35545  tendoplass  35579  tendodi1  35580  tendodi2  35581  cdlemk34  35706  cdlemk36  35709  erngdvlem3-rN  35794  tendospdi1  35817  dialss  35843  dvhvaddass  35894  dvhopvsca  35899  dvhlveclem  35905  diblss  35967  diclss  35990  diclspsn  35991  cdlemn11pre  36007  dihmeetlem12N  36115  dihmeetlem16N  36119  dihmeetlem17N  36120  dihmeetlem18N  36121  dvh4dimN  36244  lpolconN  36284  dochpolN  36287  lclkr  36330  lclkrs  36336  lcfr  36382
  Copyright terms: Public domain W3C validator