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

Theorem simpr2 962
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 956 . 2  |-  ( ( ps  /\  ch  /\  th )  ->  ch )
21adantl 452 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:  simplr2  998  simprr2  1004  simp1r2  1052  simp2r2  1058  simp3r2  1064  3anandis  1283  wereu  4405  fr3nr  4587  isopolem  5858  frfi  7118  intrnfi  7186  fisupcl  7234  cnfcomlem  7418  ackbij1lem15  7876  cofsmo  7911  sornom  7919  fpwwe2lem5  8272  supmul1  9735  xlesubadd  10599  elioc2  10729  elico2  10730  elicc2  10731  fseq1p1m1  10873  ccatswrd  11475  tanadd  12463  dvds2ln  12575  ressress  13221  f1ovscpbl  13444  mreexexlem4d  13565  mreexexd  13566  iscatd2  13599  2oppccomf  13644  issubc3  13739  fthmon  13817  fuccocl  13854  fucidcl  13855  invfuc  13864  curf2cl  14021  yonedalem4c  14067  yonedalem3  14070  pospo  14123  latjlej1  14187  latnlej2  14193  latmlem1  14203  latledi  14211  latjass  14217  latj12  14218  latj32  14219  latj13  14220  latj31  14221  latjrot  14222  latjjdi  14225  latjjdir  14226  latdisdlem  14308  prdsmndd  14421  frmdmnd  14497  grpsubrcan  14563  grpsubadd  14569  grpaddsubass  14571  grpsubsub4  14574  grppnpcan2  14575  grpnpncan  14576  mulgnndir  14605  mulgnn0dir  14606  mulgdir  14608  mulgnnass  14611  mulgnn0ass  14612  mulgass  14613  mulgsubdir  14614  pwsmulg  14625  issubg2  14652  eqgval  14682  divsgrp  14688  galcan  14774  gacan  14775  symggrp  14796  oppgmnd  14843  cmn32  15123  cmn12  15125  abladdsub  15132  mulgdi  15142  mulgsubdi  15145  dprdss  15280  dprdz  15281  dprdf1o  15283  dprdsn  15287  dprd2da  15293  dmdprdsplit  15298  ablfac1b  15321  pgpfac1lem5  15330  rngi  15369  prdsrngd  15411  opprrng  15429  mulgass3  15435  dvrass  15488  subrgunit  15579  issubrg2  15581  abvdiv  15618  lsssn0  15721  islss3  15732  prdslmodd  15742  islmhm2  15811  lspsolv  15912  islbs2  15923  islbs3  15924  lbsextlem4  15930  sralmod  15955  issubassa  16080  sraassa  16081  psrbaglesupp  16130  psrbaglecl  16131  psrbagcon  16133  psrgrp  16159  psrlmod  16162  psrrng  16171  psrassa  16174  ipdir  16559  ipdi  16560  ipsubdir  16562  ipsubdi  16563  ipass  16565  ipassr  16566  ipassr2  16567  isphld  16574  ocvlss  16588  iinopn  16664  restopnb  16922  subbascn  17000  nrmsep2  17100  isnrm3  17103  regsep2  17120  dnsconst  17122  dfcon2  17161  1stcelcls  17203  dislly  17239  ptuni2  17287  tx1stc  17360  0nelfb  17542  infil  17574  fsubbas  17578  filssufilg  17622  hauspwpwf1  17698  tmdcn2  17788  isxmet2d  17908  xmettri  17931  xmetres2  17941  bldisj  17971  blss2  17975  xmstri2  18028  mstri2  18029  xmstri  18030  mstri  18031  xmstri3  18032  mstri3  18033  msrtri  18034  comet  18075  stdbdbl  18079  met2ndci  18084  ngprcan  18147  ngplcan  18148  ngpsubcan  18151  nrgdsdi  18192  nrgdsdir  18193  nlmdsdi  18208  nlmdsdir  18209  blcvx  18320  icoopnst  18453  pi1grplem  18563  cphdivcl  18634  cphsubdir  18659  cphsubdi  18660  tchcph  18683  bcthlem5  18766  volfiniun  18920  volcn  18977  itg1val2  19055  dvconst  19282  dvlip  19356  ftc1a  19400  ulmval  19775  ulmdvlem3  19795  ang180  20128  cvxcl  20295  scvxcvx  20296  sgmmul  20456  dchrabl  20509  grpomuldivass  20932  grponpncan  20938  grpodiveq  20939  ablomuldiv  20972  ablodivdiv4  20974  ablonnncan1  20978  nvmdi  21224  nvsubadd  21229  dipassr  21440  measdivcstOLD  23566  measdivcst  23567  erdszelem9  23745  rescon  23792  cvmseu  23822  cvmlift2lem10  23858  cvmlift2lem12  23860  iseupa  23896  dedekindle  24098  frrlem4  24355  colinearalglem1  24606  axcgrtr  24615  axeuclidlem  24662  axcontlem3  24666  axcontlem4  24667  axcontlem7  24670  cgrid2  24698  segconeu  24706  btwncomim  24708  btwnswapid  24712  trisegint  24723  cgrxfr  24750  brofs2  24772  endofsegid  24780  btwnconn2  24797  seglemin  24808  segletr  24809  btwnsegle  24812  colinbtwnle  24813  broutsideof2  24817  btwnoutside  24820  broutsideof3  24821  outsideoftr  24824  outsidele  24827  fvray  24836  fvline  24839  ellines  24847  copsexgb  25069  iccss3  25237  reacomsmgrp1  25446  reacomsmgrp2  25447  reacomsmgrp3  25448  grpodrcan  25478  rltrran  25517  mvecrtol2  25580  truni1  25608  cnrsfin  25628  cnrscoa  25629  cmptdst  25671  cmptdst2  25674  usinuniopb  25697  lvsovso  25729  lvsovso3  25731  addassv  25759  icccon2  25803  isder  25810  iepiclem  25926  bosser  26270  pdiveql  26271  sdclem1  26556  sstotbnd2  26601  iscringd  26727  irrapxlem6  27015  jm2.26lem3  27197  dgrsub2  27442  mpaaroot  27463  pmtrprfv  27499  psgnunilem3  27522  matrng  27583  matassa  27584  mendrng  27603  mendlmod  27604  mendassa  27605  rfcnpre3  27807  fmuldfeq  27816  stoweidlem43  27895  stoweidlem52  27904  stoweidlem53  27905  stoweidlem56  27908  stoweidlem57  27909  stoweidlem60  27912  wlkdvspth  28366  bnj1098  29131  bnj149  29223  bnj1118  29330  lsmsat  29820  lfladdcl  29883  lflnegcl  29887  lflvscl  29889  eqlkr  29911  lshpkrlem4  29925  lshpkrlem6  29927  ldualgrplem  29957  lduallmodlem  29964  latmassOLD  30041  latm12  30042  latm32  30043  latmrot  30044  latmmdiN  30046  latmmdir  30047  omlfh1N  30070  omlfh3N  30071  cvrnbtwn2  30087  cvlexchb1  30142  cvlsupr2  30155  hlatjass  30181  hlatj12  30182  hlatj32  30183  cvrat  30233  cvrat2  30240  atltcvr  30246  atexchltN  30252  cvrat3  30253  cvrat4  30254  atbtwnexOLDN  30258  atbtwnex  30259  3dimlem3  30272  3dimlem3OLDN  30273  3at  30301  2atneat  30326  llncmp  30333  2at0mat0  30336  2atmat0  30337  llncvrlpln  30369  lplncmp  30373  2llnjaN  30377  4atlem11  30420  lplncvrlvol  30427  lvolcmp  30428  2atm2atN  30596  elpaddatriN  30614  paddasslem8  30638  paddass  30649  padd12N  30650  paddssw2  30655  paddss  30656  pmod1i  30659  pmodN  30661  pmapjlln1  30666  atmod1i1  30668  atmod1i2  30670  pexmidlem2N  30782  pl42lem2N  30791  pl42lem3N  30792  pl42lem4N  30793  pl42N  30794  lhpm0atN  30840  lautlt  30902  lautcvr  30903  lautj  30904  lautm  30905  ltrneq2  30959  cdlemd1  31009  cdleme1b  31037  cdleme1  31038  cdleme2  31039  cdleme3e  31043  cdlemefr27cl  31214  cdlemefs27cl  31224  cdleme42ke  31296  cdleme42mN  31298  cdlemf2  31373  cdlemftr2  31377  trljco  31551  tgrpgrplem  31560  tendoplass  31594  tendodi1  31595  tendodi2  31596  cdlemk34  31721  cdlemk36  31724  erngdvlem3-rN  31809  tendospdi1  31832  dialss  31858  dvhvaddass  31909  dvhopvsca  31914  dvhlveclem  31920  diblss  31982  diclss  32005  diclspsn  32006  cdlemn11pre  32022  dihmeetlem12N  32130  dihmeetlem16N  32134  dihmeetlem17N  32135  dihmeetlem18N  32136  dvh4dimN  32259  lpolconN  32299  dochpolN  32302  lclkr  32345  lclkrs  32351  lcfr  32397
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