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  4389  fr3nr  4571  isopolem  5842  frfi  7102  intrnfi  7170  fisupcl  7218  cnfcomlem  7402  ackbij1lem15  7860  cofsmo  7895  sornom  7903  fpwwe2lem5  8256  supmul1  9719  xlesubadd  10583  elioc2  10713  elico2  10714  elicc2  10715  fseq1p1m1  10857  ccatswrd  11459  tanadd  12447  dvds2ln  12559  ressress  13205  f1ovscpbl  13428  mreexexlem4d  13549  mreexexd  13550  iscatd2  13583  2oppccomf  13628  issubc3  13723  fthmon  13801  fuccocl  13838  fucidcl  13839  invfuc  13848  curf2cl  14005  yonedalem4c  14051  yonedalem3  14054  pospo  14107  latjlej1  14171  latnlej2  14177  latmlem1  14187  latledi  14195  latjass  14201  latj12  14202  latj32  14203  latj13  14204  latj31  14205  latjrot  14206  latjjdi  14209  latjjdir  14210  latdisdlem  14292  prdsmndd  14405  frmdmnd  14481  grpsubrcan  14547  grpsubadd  14553  grpaddsubass  14555  grpsubsub4  14558  grppnpcan2  14559  grpnpncan  14560  mulgnndir  14589  mulgnn0dir  14590  mulgdir  14592  mulgnnass  14595  mulgnn0ass  14596  mulgass  14597  mulgsubdir  14598  pwsmulg  14609  issubg2  14636  eqgval  14666  divsgrp  14672  galcan  14758  gacan  14759  symggrp  14780  oppgmnd  14827  cmn32  15107  cmn12  15109  abladdsub  15116  mulgdi  15126  mulgsubdi  15129  dprdss  15264  dprdz  15265  dprdf1o  15267  dprdsn  15271  dprd2da  15277  dmdprdsplit  15282  ablfac1b  15305  pgpfac1lem5  15314  rngi  15353  prdsrngd  15395  opprrng  15413  mulgass3  15419  dvrass  15472  subrgunit  15563  issubrg2  15565  abvdiv  15602  lsssn0  15705  islss3  15716  prdslmodd  15726  islmhm2  15795  lspsolv  15896  islbs2  15907  islbs3  15908  lbsextlem4  15914  sralmod  15939  issubassa  16064  sraassa  16065  psrbaglesupp  16114  psrbaglecl  16115  psrbagcon  16117  psrgrp  16143  psrlmod  16146  psrrng  16155  psrassa  16158  ipdir  16543  ipdi  16544  ipsubdir  16546  ipsubdi  16547  ipass  16549  ipassr  16550  ipassr2  16551  isphld  16558  ocvlss  16572  iinopn  16648  restopnb  16906  subbascn  16984  nrmsep2  17084  isnrm3  17087  regsep2  17104  dnsconst  17106  dfcon2  17145  1stcelcls  17187  dislly  17223  ptuni2  17271  tx1stc  17344  0nelfb  17526  infil  17558  fsubbas  17562  filssufilg  17606  hauspwpwf1  17682  tmdcn2  17772  isxmet2d  17892  xmettri  17915  xmetres2  17925  bldisj  17955  blss2  17959  xmstri2  18012  mstri2  18013  xmstri  18014  mstri  18015  xmstri3  18016  mstri3  18017  msrtri  18018  comet  18059  stdbdbl  18063  met2ndci  18068  ngprcan  18131  ngplcan  18132  ngpsubcan  18135  nrgdsdi  18176  nrgdsdir  18177  nlmdsdi  18192  nlmdsdir  18193  blcvx  18304  icoopnst  18437  pi1grplem  18547  cphdivcl  18618  cphsubdir  18643  cphsubdi  18644  tchcph  18667  bcthlem5  18750  volfiniun  18904  volcn  18961  itg1val2  19039  dvconst  19266  dvlip  19340  ftc1a  19384  ulmval  19759  ulmdvlem3  19779  ang180  20112  cvxcl  20279  scvxcvx  20280  sgmmul  20440  dchrabl  20493  grpomuldivass  20916  grponpncan  20922  grpodiveq  20923  ablomuldiv  20956  ablodivdiv4  20958  ablonnncan1  20962  nvmdi  21208  nvsubadd  21213  dipassr  21424  measdivcstOLD  23551  measdivcst  23552  erdszelem9  23730  rescon  23777  cvmseu  23807  cvmlift2lem10  23843  cvmlift2lem12  23845  iseupa  23881  dedekindle  24083  frrlem4  24284  colinearalglem1  24534  axcgrtr  24543  axeuclidlem  24590  axcontlem3  24594  axcontlem4  24595  axcontlem7  24598  cgrid2  24626  segconeu  24634  btwncomim  24636  btwnswapid  24640  trisegint  24651  cgrxfr  24678  brofs2  24700  endofsegid  24708  btwnconn2  24725  seglemin  24736  segletr  24737  btwnsegle  24740  colinbtwnle  24741  broutsideof2  24745  btwnoutside  24748  broutsideof3  24749  outsideoftr  24752  outsidele  24755  fvray  24764  fvline  24767  ellines  24775  copsexgb  24966  iccss3  25134  reacomsmgrp1  25343  reacomsmgrp2  25344  reacomsmgrp3  25345  grpodrcan  25375  rltrran  25414  mvecrtol2  25477  truni1  25505  cnrsfin  25525  cnrscoa  25526  cmptdst  25568  cmptdst2  25571  usinuniopb  25594  lvsovso  25626  lvsovso3  25628  addassv  25656  icccon2  25700  isder  25707  iepiclem  25823  bosser  26167  pdiveql  26168  sdclem1  26453  sstotbnd2  26498  iscringd  26624  irrapxlem6  26912  jm2.26lem3  27094  dgrsub2  27339  mpaaroot  27360  pmtrprfv  27396  psgnunilem3  27419  matrng  27480  matassa  27481  mendrng  27500  mendlmod  27501  mendassa  27502  rfcnpre3  27704  fmuldfeq  27713  stoweidlem43  27792  stoweidlem52  27801  stoweidlem53  27802  stoweidlem56  27805  stoweidlem57  27806  stoweidlem60  27809  bnj1098  28815  bnj149  28907  bnj1118  29014  lsmsat  29198  lfladdcl  29261  lflnegcl  29265  lflvscl  29267  eqlkr  29289  lshpkrlem4  29303  lshpkrlem6  29305  ldualgrplem  29335  lduallmodlem  29342  latmassOLD  29419  latm12  29420  latm32  29421  latmrot  29422  latmmdiN  29424  latmmdir  29425  omlfh1N  29448  omlfh3N  29449  cvrnbtwn2  29465  cvlexchb1  29520  cvlsupr2  29533  hlatjass  29559  hlatj12  29560  hlatj32  29561  cvrat  29611  cvrat2  29618  atltcvr  29624  atexchltN  29630  cvrat3  29631  cvrat4  29632  atbtwnexOLDN  29636  atbtwnex  29637  3dimlem3  29650  3dimlem3OLDN  29651  3at  29679  2atneat  29704  llncmp  29711  2at0mat0  29714  2atmat0  29715  llncvrlpln  29747  lplncmp  29751  2llnjaN  29755  4atlem11  29798  lplncvrlvol  29805  lvolcmp  29806  2atm2atN  29974  elpaddatriN  29992  paddasslem8  30016  paddass  30027  padd12N  30028  paddssw2  30033  paddss  30034  pmod1i  30037  pmodN  30039  pmapjlln1  30044  atmod1i1  30046  atmod1i2  30048  pexmidlem2N  30160  pl42lem2N  30169  pl42lem3N  30170  pl42lem4N  30171  pl42N  30172  lhpm0atN  30218  lautlt  30280  lautcvr  30281  lautj  30282  lautm  30283  ltrneq2  30337  cdlemd1  30387  cdleme1b  30415  cdleme1  30416  cdleme2  30417  cdleme3e  30421  cdlemefr27cl  30592  cdlemefs27cl  30602  cdleme42ke  30674  cdleme42mN  30676  cdlemf2  30751  cdlemftr2  30755  trljco  30929  tgrpgrplem  30938  tendoplass  30972  tendodi1  30973  tendodi2  30974  cdlemk34  31099  cdlemk36  31102  erngdvlem3-rN  31187  tendospdi1  31210  dialss  31236  dvhvaddass  31287  dvhopvsca  31292  dvhlveclem  31298  diblss  31360  diclss  31383  diclspsn  31384  cdlemn11pre  31400  dihmeetlem12N  31508  dihmeetlem16N  31512  dihmeetlem17N  31513  dihmeetlem18N  31514  dvh4dimN  31637  lpolconN  31677  dochpolN  31680  lclkr  31723  lclkrs  31729  lcfr  31775
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