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

Theorem simpr2 1004
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 998 . 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 974
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 976
This theorem is referenced by:  simplr2  1040  simprr2  1046  simp1r2  1094  simp2r2  1100  simp3r2  1106  3anandis  1331  wereu  4865  isopolem  6226  fr3nr  6600  frfi  7767  intrnfi  7878  fisupcl  7930  cnfcomlem  8146  cnfcomlemOLD  8154  ackbij1lem15  8617  cofsmo  8652  sornom  8660  fpwwe2lem5  9015  dedekindle  9748  supmul1  10514  eluzuzle  11098  xlesubadd  11464  elioc2  11596  elico2  11597  elicc2  11598  fseq1p1m1  11761  fz0fzelfz0  11788  swrdsymbeq  12651  ccatswrd  12660  swrdswrdlem  12663  tanadd  13779  dvds2ln  13891  cshwsidrepsw  14455  ressress  14571  f1ovscpbl  14800  mreexexlem4d  14921  mreexexd  14922  iscatd2  14955  2oppccomf  14997  issubc3  15092  fthmon  15170  fuccocl  15207  fucidcl  15208  invfuc  15217  curf2cl  15374  yonedalem4c  15420  yonedalem3  15423  pospo  15477  latjle12  15566  latjlej1  15569  latnlej2  15575  latlem12  15582  latmlem1  15585  latledi  15593  latjass  15599  latj12  15600  latj32  15601  latj13  15602  latj31  15603  latjrot  15604  latjjdi  15607  latjjdir  15608  latdisdlem  15693  prdsmndd  15827  frmdmnd  15901  grpsubrcan  15993  grpsubadd  16000  grpaddsubass  16002  grpsubsub4  16005  grppnpcan2  16006  grpnpncan  16007  mulgnndir  16038  mulgnn0dir  16039  mulgdir  16041  mulgnnass  16044  mulgnn0ass  16045  mulgass  16046  mulgsubdir  16047  pwsmulg  16058  issubg2  16090  eqgval  16124  qusgrp  16130  galcan  16216  gacan  16217  oppgmnd  16263  symggrp  16299  fvcosymgeq  16328  pmtrprfv  16352  psgnunilem3  16395  cmn32  16690  cmn12  16692  abladdsub  16699  mulgdi  16709  mulgsubdi  16712  dprdss  16950  dprdz  16951  dprdf1o  16953  dprdsn  16957  dprd2da  16965  dmdprdsplit  16970  ablfac1b  16995  pgpfac1lem5  17004  srgi  17037  srgbinom  17070  ringi  17085  prdsringd  17135  opprring  17154  mulgass3  17160  dvrass  17213  subrgunit  17321  issubrg2  17323  abvdiv  17360  lsssn0  17468  islss3  17479  prdslmodd  17489  islmhm2  17558  lspsolv  17663  islbs2  17674  islbs3  17675  lbsextlem4  17681  sralmod  17707  issubassa  17847  sraassa  17848  psrbaglesupp  17891  psrbaglesuppOLD  17892  psrbaglecl  17893  psrbagcon  17896  psrgrp  17925  psrlmod  17928  psrring  17940  psrassa  17943  psgndiflemB  18509  ipdir  18547  ipdi  18548  ipsubdir  18550  ipsubdi  18551  ipass  18553  ipassr  18554  ipassr2  18555  isphld  18562  ocvlss  18576  mamudm  18763  matring  18818  matassa  18819  ofco2  18826  ma1repveval  18946  mdetunilem1  18987  mdetunilem9  18995  chpscmatgsumbin  19218  iinopn  19284  restopnb  19549  subbascn  19628  nrmsep2  19730  isnrm3  19733  regsep2  19750  dnsconst  19752  dfcon2  19793  1stcelcls  19835  dislly  19871  ptuni2  19950  tx1stc  20024  0nelfb  20205  infil  20237  fsubbas  20241  filssufilg  20285  hauspwpwf1  20361  cnextcn  20440  tmdcn2  20461  ustuqtoplem  20615  utopsnneiplem  20623  psmettri  20688  isxmet2d  20703  xmettri  20727  xmetres2  20737  bldisj  20774  blss2ps  20779  blss2  20780  xmstri2  20842  mstri2  20843  xmstri  20844  mstri  20845  xmstri3  20846  mstri3  20847  msrtri  20848  comet  20889  stdbdbl  20893  met2ndci  20898  ngprcan  21002  ngplcan  21003  ngpsubcan  21006  nrgdsdi  21047  nrgdsdir  21048  nlmdsdi  21063  nlmdsdir  21064  blcvx  21176  icoopnst  21312  pi1grplem  21422  cvsdiv  21482  cvsdivcl  21483  cphdivcl  21502  cphsubdir  21527  cphsubdi  21528  tchcph  21553  bcthlem5  21640  volfiniun  21830  volcn  21888  itg1val2  21964  dvconst  22193  dvlip  22267  ftc1a  22311  ulmval  22647  ulmdvlem3  22669  ang180  23018  cvxcl  23186  scvxcvx  23187  sgmmul  23348  dchrabl  23401  motgrp  23802  f1otrge  24047  colinearalglem1  24081  axcgrtr  24090  axeuclidlem  24137  axcontlem3  24141  axcontlem4  24142  axcontlem7  24145  eengtrkg  24160  eengtrkge  24161  isspthonpth  24458  wlkdvspth  24482  clwlkfoclwwlk  24717  el2spthonot0  24743  el2wlkonotot0  24744  usg2wotspth  24756  2spontn0vne  24759  rusgranumwlks  24828  rusgranumwwlkg  24831  iseupa  24837  3vfriswmgra  24877  frgrareggt1  24988  grpomuldivass  25123  grponpncan  25129  grpodiveq  25130  ablomuldiv  25163  ablodivdiv4  25165  ablonnncan1  25169  nvmdi  25417  nvsubadd  25422  dipassr  25633  archiabllem2c  27612  dvrdir  27653  dvrcan5  27656  reofld  27703  pstmfval  27748  qqhval2lem  27835  qqhvq  27841  measdivcstOLD  28068  measdivcst  28069  erdszelem9  28516  rescon  28564  cvmseu  28594  cvmlift2lem10  28630  cvmlift2lem12  28632  elmrsubrn  28753  mclsind  28803  frrlem4  29365  cgrid2  29628  segconeu  29636  btwncomim  29638  btwnswapid  29642  trisegint  29653  cgrxfr  29680  brofs2  29702  endofsegid  29710  btwnconn2  29727  seglemin  29738  segletr  29739  btwnsegle  29742  colinbtwnle  29743  broutsideof2  29747  btwnoutside  29750  broutsideof3  29751  outsideoftr  29754  outsidele  29757  fvray  29766  fvline  29769  ellines  29777  ftc1anc  30073  sdclem1  30211  sstotbnd2  30245  iscringd  30371  irrapxlem6  30738  jm2.26lem3  30918  dgrsub2  31059  mpaaroot  31080  mendring  31117  mendlmod  31118  mendassa  31119  rfcnpre3  31362  fmuldfeq  31505  stoweidlem43  31714  stoweidlem52  31723  stoweidlem53  31724  stoweidlem56  31727  stoweidlem57  31728  stoweidlem60  31731  ltsubsubaddltsub  32162  copissgrp  32333  cznrng  32473  funcringcsetcOLD2lem9  32589  funcringcsetclem9OLD  32612  ldepsprlem  32808  lincresunit3  32817  lincreslvec3  32818  bnj1098  33575  bnj149  33666  bnj1118  33773  lsmsat  34473  lfladdcl  34536  lflnegcl  34540  lflvscl  34542  eqlkr  34564  lshpkrlem4  34578  lshpkrlem6  34580  ldualgrplem  34610  lduallmodlem  34617  latmassOLD  34694  latm12  34695  latm32  34696  latmrot  34697  latmmdiN  34699  latmmdir  34700  omlfh1N  34723  omlfh3N  34724  cvrnbtwn2  34740  cvlexchb1  34795  cvlsupr2  34808  hlatjass  34834  hlatj12  34835  hlatj32  34836  cvrat  34886  cvrat2  34893  atltcvr  34899  atexchltN  34905  cvrat3  34906  cvrat4  34907  atbtwnexOLDN  34911  atbtwnex  34912  3dimlem3  34925  3dimlem3OLDN  34926  3at  34954  2atneat  34979  llncmp  34986  2at0mat0  34989  2atmat0  34990  llncvrlpln  35022  lplncmp  35026  2llnjaN  35030  4atlem11  35073  lplncvrlvol  35080  lvolcmp  35081  2atm2atN  35249  elpaddatriN  35267  paddasslem8  35291  paddass  35302  padd12N  35303  paddssw2  35308  paddss  35309  pmod1i  35312  pmodN  35314  pmapjlln1  35319  atmod1i1  35321  atmod1i2  35323  pexmidlem2N  35435  pl42lem2N  35444  pl42lem3N  35445  pl42lem4N  35446  pl42N  35447  lhpm0atN  35493  lautlt  35555  lautcvr  35556  lautj  35557  lautm  35558  ltrneq2  35612  cdlemd1  35663  cdleme1b  35691  cdleme1  35692  cdleme2  35693  cdleme3e  35697  cdlemefr27cl  35869  cdlemefs27cl  35879  cdleme42ke  35951  cdleme42mN  35953  cdlemf2  36028  cdlemftr2  36032  trljco  36206  tgrpgrplem  36215  tendoplass  36249  tendodi1  36250  tendodi2  36251  cdlemk34  36376  cdlemk36  36379  erngdvlem3-rN  36464  tendospdi1  36487  dialss  36513  dvhvaddass  36564  dvhopvsca  36569  dvhlveclem  36575  diblss  36637  diclss  36660  diclspsn  36661  cdlemn11pre  36677  dihmeetlem12N  36785  dihmeetlem16N  36789  dihmeetlem17N  36790  dihmeetlem18N  36791  dvh4dimN  36914  lpolconN  36954  dochpolN  36957  lclkr  37000  lclkrs  37006  lcfr  37052
  Copyright terms: Public domain W3C validator