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

Theorem simpr2 964
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 958 . 2  |-  ( ( ps  /\  ch  /\  th )  ->  ch )
21adantl 453 1  |-  ( (
ph  /\  ( ps  /\ 
ch  /\  th )
)  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    /\ w3a 936
This theorem is referenced by:  simplr2  1000  simprr2  1006  simp1r2  1054  simp2r2  1060  simp3r2  1066  3anandis  1285  wereu  4578  fr3nr  4760  isopolem  6065  frfi  7352  intrnfi  7421  fisupcl  7472  cnfcomlem  7656  ackbij1lem15  8114  cofsmo  8149  sornom  8157  fpwwe2lem5  8509  supmul1  9973  xlesubadd  10842  elioc2  10973  elico2  10974  elicc2  10975  fseq1p1m1  11122  ccatswrd  11773  tanadd  12768  dvds2ln  12880  ressress  13526  f1ovscpbl  13751  mreexexlem4d  13872  mreexexd  13873  iscatd2  13906  2oppccomf  13951  issubc3  14046  fthmon  14124  fuccocl  14161  fucidcl  14162  invfuc  14171  curf2cl  14328  yonedalem4c  14374  yonedalem3  14377  pospo  14430  latjlej1  14494  latnlej2  14500  latmlem1  14510  latledi  14518  latjass  14524  latj12  14525  latj32  14526  latj13  14527  latj31  14528  latjrot  14529  latjjdi  14532  latjjdir  14533  latdisdlem  14615  prdsmndd  14728  frmdmnd  14804  grpsubrcan  14870  grpsubadd  14876  grpaddsubass  14878  grpsubsub4  14881  grppnpcan2  14882  grpnpncan  14883  mulgnndir  14912  mulgnn0dir  14913  mulgdir  14915  mulgnnass  14918  mulgnn0ass  14919  mulgass  14920  mulgsubdir  14921  pwsmulg  14932  issubg2  14959  eqgval  14989  divsgrp  14995  galcan  15081  gacan  15082  symggrp  15103  oppgmnd  15150  cmn32  15430  cmn12  15432  abladdsub  15439  mulgdi  15449  mulgsubdi  15452  dprdss  15587  dprdz  15588  dprdf1o  15590  dprdsn  15594  dprd2da  15600  dmdprdsplit  15605  ablfac1b  15628  pgpfac1lem5  15637  rngi  15676  prdsrngd  15718  opprrng  15736  mulgass3  15742  dvrass  15795  subrgunit  15886  issubrg2  15888  abvdiv  15925  lsssn0  16024  islss3  16035  prdslmodd  16045  islmhm2  16114  lspsolv  16215  islbs2  16226  islbs3  16227  lbsextlem4  16233  sralmod  16258  issubassa  16383  sraassa  16384  psrbaglesupp  16433  psrbaglecl  16434  psrbagcon  16436  psrgrp  16462  psrlmod  16465  psrrng  16474  psrassa  16477  ipdir  16870  ipdi  16871  ipsubdir  16873  ipsubdi  16874  ipass  16876  ipassr  16877  ipassr2  16878  isphld  16885  ocvlss  16899  iinopn  16975  restopnb  17239  subbascn  17318  nrmsep2  17420  isnrm3  17423  regsep2  17440  dnsconst  17442  dfcon2  17482  1stcelcls  17524  dislly  17560  ptuni2  17608  tx1stc  17682  0nelfb  17863  infil  17895  fsubbas  17899  filssufilg  17943  hauspwpwf1  18019  cnextcn  18098  tmdcn2  18119  ustuqtoplem  18269  utopsnneiplem  18277  psmettri  18342  isxmet2d  18357  xmettri  18381  xmetres2  18391  bldisj  18428  blss2ps  18433  blss2  18434  xmstri2  18496  mstri2  18497  xmstri  18498  mstri  18499  xmstri3  18500  mstri3  18501  msrtri  18502  comet  18543  stdbdbl  18547  met2ndci  18552  ngprcan  18656  ngplcan  18657  ngpsubcan  18660  nrgdsdi  18701  nrgdsdir  18702  nlmdsdi  18717  nlmdsdir  18718  blcvx  18829  icoopnst  18964  pi1grplem  19074  cphdivcl  19145  cphsubdir  19170  cphsubdi  19171  tchcph  19194  bcthlem5  19281  volfiniun  19441  volcn  19498  itg1val2  19576  dvconst  19803  dvlip  19877  ftc1a  19921  ulmval  20296  ulmdvlem3  20318  ang180  20656  cvxcl  20823  scvxcvx  20824  sgmmul  20985  dchrabl  21038  isspthonpth  21584  wlkdvspth  21608  iseupa  21687  grpomuldivass  21837  grponpncan  21843  grpodiveq  21844  ablomuldiv  21877  ablodivdiv4  21879  ablonnncan1  21883  nvmdi  22131  nvsubadd  22136  dipassr  22347  dvrdir  24226  dvrcan5  24229  reofld  24280  pstmfval  24291  qqhval2lem  24365  qqhvq  24371  measdivcstOLD  24578  measdivcst  24579  erdszelem9  24885  rescon  24933  cvmseu  24963  cvmlift2lem10  24999  cvmlift2lem12  25001  dedekindle  25188  frrlem4  25585  colinearalglem1  25845  axcgrtr  25854  axeuclidlem  25901  axcontlem3  25905  axcontlem4  25906  axcontlem7  25909  cgrid2  25937  segconeu  25945  btwncomim  25947  btwnswapid  25951  trisegint  25962  cgrxfr  25989  brofs2  26011  endofsegid  26019  btwnconn2  26036  seglemin  26047  segletr  26048  btwnsegle  26051  colinbtwnle  26052  broutsideof2  26056  btwnoutside  26059  broutsideof3  26060  outsideoftr  26063  outsidele  26066  fvray  26075  fvline  26078  ellines  26086  ftc1anc  26288  sdclem1  26447  sstotbnd2  26483  iscringd  26609  irrapxlem6  26890  jm2.26lem3  27072  dgrsub2  27316  mpaaroot  27337  pmtrprfv  27373  psgnunilem3  27396  matrng  27457  matassa  27458  mendrng  27477  mendlmod  27478  mendassa  27479  rfcnpre3  27680  fmuldfeq  27689  stoweidlem43  27768  stoweidlem52  27777  stoweidlem53  27778  stoweidlem56  27781  stoweidlem57  27782  stoweidlem60  27785  uzletr  28103  fz0fzelfz0  28118  swdeq  28196  swrdswrdlem  28198  cshwidxmod  28243  2cshw1lem2  28249  el2spthonot0  28338  usg2wotspth  28351  2spontn0vne  28354  3vfriswmgra  28395  bnj1098  29154  bnj149  29246  bnj1118  29353  lsmsat  29806  lfladdcl  29869  lflnegcl  29873  lflvscl  29875  eqlkr  29897  lshpkrlem4  29911  lshpkrlem6  29913  ldualgrplem  29943  lduallmodlem  29950  latmassOLD  30027  latm12  30028  latm32  30029  latmrot  30030  latmmdiN  30032  latmmdir  30033  omlfh1N  30056  omlfh3N  30057  cvrnbtwn2  30073  cvlexchb1  30128  cvlsupr2  30141  hlatjass  30167  hlatj12  30168  hlatj32  30169  cvrat  30219  cvrat2  30226  atltcvr  30232  atexchltN  30238  cvrat3  30239  cvrat4  30240  atbtwnexOLDN  30244  atbtwnex  30245  3dimlem3  30258  3dimlem3OLDN  30259  3at  30287  2atneat  30312  llncmp  30319  2at0mat0  30322  2atmat0  30323  llncvrlpln  30355  lplncmp  30359  2llnjaN  30363  4atlem11  30406  lplncvrlvol  30413  lvolcmp  30414  2atm2atN  30582  elpaddatriN  30600  paddasslem8  30624  paddass  30635  padd12N  30636  paddssw2  30641  paddss  30642  pmod1i  30645  pmodN  30647  pmapjlln1  30652  atmod1i1  30654  atmod1i2  30656  pexmidlem2N  30768  pl42lem2N  30777  pl42lem3N  30778  pl42lem4N  30779  pl42N  30780  lhpm0atN  30826  lautlt  30888  lautcvr  30889  lautj  30890  lautm  30891  ltrneq2  30945  cdlemd1  30995  cdleme1b  31023  cdleme1  31024  cdleme2  31025  cdleme3e  31029  cdlemefr27cl  31200  cdlemefs27cl  31210  cdleme42ke  31282  cdleme42mN  31284  cdlemf2  31359  cdlemftr2  31363  trljco  31537  tgrpgrplem  31546  tendoplass  31580  tendodi1  31581  tendodi2  31582  cdlemk34  31707  cdlemk36  31710  erngdvlem3-rN  31795  tendospdi1  31818  dialss  31844  dvhvaddass  31895  dvhopvsca  31900  dvhlveclem  31906  diblss  31968  diclss  31991  diclspsn  31992  cdlemn11pre  32008  dihmeetlem12N  32116  dihmeetlem16N  32120  dihmeetlem17N  32121  dihmeetlem18N  32122  dvh4dimN  32245  lpolconN  32285  dochpolN  32288  lclkr  32331  lclkrs  32337  lcfr  32383
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 178  df-an 361  df-3an 938
  Copyright terms: Public domain W3C validator