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

Theorem simpr3 963
Description: Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.)
Assertion
Ref Expression
simpr3  |-  ( (
ph  /\  ( ps  /\ 
ch  /\  th )
)  ->  th )

Proof of Theorem simpr3
StepHypRef Expression
1 simp3 957 . 2  |-  ( ( ps  /\  ch  /\  th )  ->  th )
21adantl 452 1  |-  ( (
ph  /\  ( ps  /\ 
ch  /\  th )
)  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934
This theorem is referenced by:  simplr3  999  simprr3  1005  simp1r3  1053  simp2r3  1059  simp3r3  1065  3anandis  1283  fr3nr  4587  isopolem  5858  elfir  7185  intrnfi  7186  fisupcl  7234  cnfcomlem  7418  ackbij1lem15  7876  pwfseqlem4a  8299  pwfseqlem4  8300  xlesubadd  10599  elioc2  10729  elico2  10730  elicc2  10731  fseq1p1m1  10873  ccatswrd  11475  tanadd  12463  dvds2ln  12575  ressress  13221  f1ovscpbl  13444  mreexexlem4d  13565  mreexexd  13566  2oppccomf  13644  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  imasmnd2  14425  imasmnd  14426  frmdmnd  14497  grpsubadd  14569  grpaddsubass  14571  grpsubsub4  14574  grppnpcan2  14575  grpnpncan  14576  grpnnncan2  14577  mulgnndir  14605  mulgnn0dir  14606  mulgnnass  14611  mulgnn0ass  14612  mulgass  14613  pwsmulg  14625  imasgrp2  14626  imasgrp  14627  issubg2  14652  divsgrp  14688  galcan  14774  gacan  14775  symggrp  14796  oppgmnd  14843  frgp0  15085  cmn32  15123  cmn12  15125  abladdsub  15132  mulgdi  15142  mulgsubdi  15145  dprdss  15280  dprdf1o  15283  dprdsn  15287  dmdprdsplit  15298  pgpfac1lem5  15330  rngi  15369  prdsrngd  15411  imasrng  15418  opprrng  15429  mulgass3  15435  dvrass  15488  subrgunit  15579  issubrg2  15581  abvdiv  15618  lss1  15712  lsssn0  15721  islss3  15732  prdslmodd  15742  islmhm2  15811  lspsolv  15912  lbsextlem4  15930  sralmod  15955  issubassa  16080  sraassa  16081  psrbaglesupp  16130  psrbagcon  16133  psrgrp  16159  psrlmod  16162  psrrng  16171  psrassa  16174  mpllsslem  16196  ipdi  16560  ipsubdir  16562  ipsubdi  16563  ipassr  16566  ipassr2  16567  isphld  16574  ocvlss  16588  iinopn  16664  restopnb  16922  subbascn  17000  nrmsep2  17100  isnrm3  17103  t1sep  17114  regsep2  17120  dnsconst  17122  dfcon2  17161  dislly  17239  tx1stc  17360  qtophmeo  17524  filss  17564  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  met2ndci  18084  ngprcan  18147  ngplcan  18148  ngpsubcan  18151  nrgdsdi  18192  nrgdsdir  18193  nlmdsdi  18208  nlmdsdir  18209  blcvx  18320  iocopnst  18454  icccvx  18464  pi1grplem  18563  pi1xfrf  18567  pi1cof  18573  cphdivcl  18634  cphsubdir  18659  cphsubdi  18660  bcthlem5  18766  volfiniun  18920  volcn  18977  itg1val2  19055  dvconst  19282  dvlip  19356  ftc1a  19400  ulmdvlem3  19795  ang180  20128  cvxcl  20295  scvxcvx  20296  sgmmul  20456  logexprlim  20480  dchrabl  20509  grpomuldivass  20932  grpopnpcan2  20936  grponpncan  20938  grpodiveq  20939  ablodivdiv4  20974  ablonnncan  20976  ismndo1  21027  nvsubadd  21229  dipdi  21437  dipsubdi  21443  disjdsct  23384  esumcvg  23469  measdivcstOLD  23566  measdivcst  23567  erdszelem9  23745  cvmseu  23822  colinearalglem1  24606  colinearalg  24610  axcgrtr  24615  axlowdimlem16  24657  axeuclidlem  24662  axcontlem4  24667  axcontlem7  24670  axcontlem12  24675  cgrid2  24698  btwncomim  24708  btwnswapid  24712  trisegint  24723  cgrxfr  24750  btwnxfr  24751  brofs2  24772  brifs2  24773  endofsegid  24780  btwnconn1lem11  24792  btwnconn2  24797  segcon2  24800  seglemin  24808  segletr  24809  btwnsegle  24812  colinbtwnle  24813  broutsideof2  24817  btwnoutside  24820  broutsideof3  24821  outsideoftr  24824  outsidele  24827  ellines  24847  linethrueu  24851  copsexgb  25069  iccss3  25237  reacomsmgrp2  25447  reacomsmgrp3  25448  grpodlcan  25479  rltrran  25517  dblsubvec  25577  mvecrtol2  25580  cnrsfin  25628  cnrscoa  25629  cmptdst  25671  cmptdst2  25674  usinuniopb  25697  lvsovso  25729  addassv  25759  icccon2  25803  iepiclem  25926  cmpsubc  25959  sdclem1  26556  sstotbnd2  26601  zerdivemp1x  26689  isdrngo2  26692  iscringd  26727  irrapxlem6  27015  jm2.26lem3  27197  mpaamn  27464  pmtrprfv  27499  psgnunilem3  27522  matrng  27583  matassa  27584  mendrng  27603  mendlmod  27604  mendassa  27605  rfcnpre4  27808  fmuldfeq  27816  stoweidlem43  27895  stoweidlem52  27904  stoweidlem53  27905  stoweidlem56  27908  wlkdvspth  28366  bnj970  29295  bnj910  29296  lsmsat  29820  lfladdcl  29883  lflnegcl  29887  lflvscl  29889  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  cvlexch3  30144  cvlexch4N  30145  cvlatexchb1  30146  cvlsupr2  30155  hlatjass  30181  hlatj12  30182  hlatj32  30183  cvrat  30233  atcvrj0  30239  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  islpln2a  30359  llncvrlpln  30369  lplncmp  30373  3atnelvolN  30397  4atlem11  30420  lplncvrlvol  30427  lvolcmp  30428  2atm2atN  30596  elpaddatriN  30614  elpadd2at2  30618  paddasslem8  30638  paddasslem17  30647  paddass  30649  padd12N  30650  paddssw1  30654  pmodlem2  30658  pmodN  30661  pmapjlln1  30666  atmod1i2  30670  pexmidlem2N  30782  pexmidlem7N  30787  pl42lem2N  30791  pl42lem3N  30792  pl42lem4N  30793  pl42N  30794  lhp2lt  30812  lhpm0atN  30840  lautlt  30902  lautcvr  30903  lautj  30904  lautm  30905  ltrneq2  30959  cdleme1b  31037  cdleme3b  31040  cdleme3c  31041  cdleme9b  31063  cdlemefs27cl  31224  cdleme42mN  31298  cdlemg4c  31423  trljco  31551  tgrpgrplem  31560  tendoplass  31594  tendodi1  31595  tendodi2  31596  erngplus2  31615  erngplus2-rN  31623  cdlemk36  31724  erngdvlem3  31801  erngdvlem3-rN  31809  dvaplusgv  31821  tendospass  31831  tendospdi1  31832  dvalveclem  31837  dialss  31858  dvhvaddass  31909  dvhopvsca  31914  dvhlveclem  31920  diblss  31982  diclss  32005  diclspsn  32006  cdlemn11pre  32022  dihmeetlem12N  32130  dihmeetlem16N  32134  dihmeetlem17N  32135  dvh4dimN  32259  lpolsatN  32300  lpolpolsatN  32301  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