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

Theorem simplrr 769
Description: Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.)
Assertion
Ref Expression
simplrr  |-  ( ( ( ph  /\  ( ps  /\  ch ) )  /\  th )  ->  ch )

Proof of Theorem simplrr
StepHypRef Expression
1 simpr 462 . 2  |-  ( ( ps  /\  ch )  ->  ch )
21ad2antlr 731 1  |-  ( ( ( ph  /\  ( ps  /\  ch ) )  /\  th )  ->  ch )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370
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 188  df-an 372
This theorem is referenced by:  pm2.61da3neOLD  2752  rmob  3397  disjxiun  4423  fsnex  6196  f1prex  6197  isotr  6242  weniso  6260  riota5f  6291  tfrlem9a  7112  oaass  7270  oeeui  7311  oaabs2  7354  resixpfo  7568  omxpenlem  7679  pw2f1olem  7682  fopwdom  7686  fofinf1o  7858  marypha1lem  7953  ordiso2  8030  oismo  8055  ixpiunwdom  8106  cantnf  8197  fseqenlem1  8453  iunfictbso  8543  dfac12lem2  8572  dfac12lem3  8573  infunsdom1  8641  infpssrlem5  8735  fin23lem24  8750  isf32lem2  8782  isf32lem4  8784  isf34lem4  8805  fin1a2lem12  8839  fin1a2lem13  8840  ttukeylem6  8942  fpwwe2lem12  9065  fpwwe2lem13  9066  fpwwe2  9067  winalim2  9120  wunex2  9162  tskord  9204  prlem934  9457  mulcmpblnr  9494  dedekind  9796  addid1  9812  cnegex  9813  negeu  9864  add20  10125  divdivdiv  10307  ltmul12a  10460  lemul12a  10462  lediv12a  10499  supaddc  10574  supmul1  10576  cru  10601  uzwo3  11259  xleadd1a  11539  xmullem  11550  xmulgt0  11569  xlemul1a  11574  ixxun  11651  ixxss12  11655  ioodisj  11760  fz0fzelfz0  11894  mulexpz  12309  leexp1a  12328  expmulnbnd  12401  hashf1  12615  brfi1uzind  12641  reuccats1  12822  abs3lem  13380  rexanre  13388  cau3lem  13396  limsupgre  13520  limsupgreOLD  13521  limsupbnd2  13524  limsupbnd2OLD  13525  o1lo1  13579  rlimclim1  13587  rlimclim  13588  rlimcn1  13630  rlimcn2  13632  o1of2  13654  o1rlimmul  13660  lo1add  13668  lo1mul  13669  isercolllem1  13706  climcau  13712  caucvgrlem  13714  caucvgrlemOLD  13715  caucvgb  13724  summolem2  13760  summo  13761  modfsummod  13832  o1fsum  13851  prodmolem2  13967  isprm5  14613  isprm6  14628  rpdvds  14638  pclem  14742  pcqmul  14757  pcexp  14763  pcneg  14777  pcprmpw2  14785  pcadd  14788  pcmpt  14791  4sqlem13OLD  14855  4sqlem13  14861  vdwlem2  14886  vdwlem7  14891  vdwlem12  14896  ramval  14914  ramvalOLD  14915  ramub2  14925  ramz2  14936  ramcl  14941  cshwshashlem2  15021  imasval  15359  imasdsval  15363  mreexexd  15496  acsfn  15507  issubc3  15696  idfucl  15728  funcres2c  15748  isnat  15794  fucpropd  15824  xpcval  16004  xpcco  16010  prfval  16026  evlf2  16045  evlfcl  16049  curf12  16054  curf1cl  16055  curf2  16056  curfcl  16059  curf2ndf  16074  hof2val  16083  hofcl  16086  hofpropd  16094  yonedalem4a  16102  yonedainv  16108  drsdirfi  16125  pospo  16161  poslubmo  16334  posglbmo  16335  isipodrs  16349  acsinfd  16368  gsumvalx  16455  gsumpropd2lem  16458  ismndd  16501  mndpropd  16504  mhmeql  16553  mrcmndind  16555  frmdup3lem  16592  mhmmnd  16750  issubg4  16778  ssnmz  16801  conjnmzb  16859  f1otrspeq  17030  psgneu  17089  pgpfi  17183  sylow2blem3  17200  slwhash  17202  fislw  17203  sylow3lem2  17206  lsmdisj2  17258  pj1eu  17272  efgredlem  17323  frgpuplem  17348  gexex  17417  frgpnabl  17437  dprdfadd  17579  dpjidcl  17617  pgpfac1lem3  17636  pgpfaclem3  17642  ablfac2  17648  ringpropd  17738  islmhm2  18187  lmhmpropd  18222  lbsextlem4  18310  assapropd  18477  psrval  18512  evlslem1  18664  prmirredlem  18986  psgndiflemA  19091  lsmcss  19177  uvcf1  19272  frlmsslsp  19276  frlmup1  19278  mamucl  19348  mamuass  19349  mamudi  19350  mamudir  19351  mamuvs1  19352  mamuvs2  19353  mamulid  19388  mamurid  19389  dmatsubcl  19445  dmatmulcl  19447  scmatscm  19460  marrepval  19509  marepveval  19515  mdetunilem7  19565  gsummatr01lem4  19605  cpmatmcllem  19664  mat2pmatf1  19675  mat2pmatlin  19681  decpmatmul  19718  pm2mpmhmlem2  19765  chpidmat  19793  pptbas  19945  toponmre  20031  restbas  20096  iscncl  20207  cnrest2  20224  cnpdis  20231  lmcnp  20242  dishaus  20320  cmpcovf  20328  tgcmp  20338  dfcon2  20356  clscon  20367  2ndcctbss  20392  dis2ndc  20397  1stccnp  20399  islly2  20421  cldllycmp  20432  locfincmp  20463  comppfsc  20469  kgentopon  20475  txcls  20541  ptpjopn  20549  dfac14  20555  xkoccn  20556  txcnp  20557  txcmpb  20581  txlm  20585  xkopt  20592  xkoco1cn  20594  xkoco2cn  20595  qtopcn  20651  qtoprest  20654  regr1lem2  20677  xkocnv  20751  qtophmeo  20754  fmfnfmlem4  20894  hausflim  20918  hauspwpwf1  20924  fclscmp  20967  alexsublem  20981  alexsubALTlem2  20985  alexsubALTlem3  20986  ptcmplem3  20991  ptcmplem4  20992  ptcmplem5  20993  cnextfun  21001  tmdgsum2  21033  symgtgp  21038  tsmsval2  21066  tsmsgsum  21075  utoptop  21171  ismet2  21270  blin  21358  metss2lem  21448  methaus  21457  met1stc  21458  met2ndci  21459  prdsxmslem2  21466  metcnp3  21477  metcnpi3  21483  metustto  21490  metustfbas  21494  nlmvscn  21612  nrginvrcn  21616  xrsxmet  21729  reconnlem1  21746  reconn  21748  xrge0tsms  21754  xmetdcn2  21757  metdscn  21775  addcnlem  21783  fsumcn  21789  cnheiborlem  21869  cnheibor  21870  bndth  21873  lebnum  21879  nmoleub2lem2  22014  ipcn  22101  iscmet3  22147  caubl  22161  rrxdstprj1  22247  minveclem3b  22254  minveclem7  22261  pjthlem2  22264  pmltpc  22273  volfiniun  22368  ioombl1  22383  dyadss  22420  dyaddisjlem  22421  dyadmax  22424  dyadmbllem  22425  opnmbllem  22427  itg1addlem2  22523  itg10a  22536  mbfi1fseqlem6  22546  itg2seq  22568  itg2monolem1  22576  itg2gt0  22586  itgfsum  22652  limcfval  22695  ellimc2  22700  ellimc3  22702  limcres  22709  limciun  22717  dvres  22734  dveflem  22799  rolle  22810  dvlip2  22815  c1liplem1  22816  dvgt0lem1  22822  dvgt0  22824  dvlt0  22825  dvne0  22831  dvfsumrlimge0  22850  ftc1lem6  22861  itgsubst  22869  mdegmullem  22895  ply1domn  22940  ply1divex  22953  fta1g  22984  fta1b  22986  plyf  23011  dgrlem  23042  coeid  23051  plydivalg  23111  aannenlem1  23140  aalioulem3  23146  aalioulem6  23149  abelthlem8  23250  efif1olem4  23350  chordthm  23619  xrlimcnp  23750  jensen  23770  lgamcvglem  23821  lgamcvg2  23836  sqf11  23920  fsumvma2  23996  perfectlem2  24012  lgsdilem  24104  lgsquad2lem2  24141  lgsquad3  24143  2sqlem5  24150  2sqlem9  24155  2sqb  24160  rpvmasumlem  24179  dchrisum0flb  24202  dchrisum0  24212  pntpbnd  24280  pntibndlem3  24284  pntleml  24303  legov  24481  legtrid  24487  tglinethru  24531  tglnpt2  24536  tglineintmo  24537  mirreu3  24550  perpcom  24606  colperpexlem3  24622  mideu  24628  opphllem1  24637  lnopp2hpgb  24652  trgcopy  24693  brcgr  24767  brbtwn2  24772  colinearalg  24777  axsegcon  24794  axeuclidlem  24829  axcontlem9  24839  ecgrtg  24850  elntg  24851  eengtrkg  24852  cusgrarn  25023  usgrasscusgra  25047  4cycl4dv4e  25232  wwlkext2clwwlk  25367  usg2spthonot1  25454  usgfidegfi  25474  eupath2  25544  usg2spot2nb  25629  numclwwlk6  25677  vacn  26166  blocni  26282  ubthlem3  26350  minvecolem7  26361  chocunii  26780  pjhthmo  26781  pjhthlem2  26871  kbass5  27599  mdsymlem5  27886  foresf1o  27966  fcobij  28144  xrofsup  28180  archirngz  28335  archiabllem2a  28340  xrge0tsmsd  28378  isarchiofld  28410  smatrcl  28452  reff  28496  ordtconlem1  28560  qqhval2  28616  volmeas  28884  fiunelcarsg  28968  ballotlemfc0  29142  ballotlemfcc  29143  signstfvneq0  29240  derangenlem  29673  erdsze2lem1  29705  pconcon  29733  conpcon  29737  cvxscon  29745  cvmliftmolem2  29784  cvmliftmo  29786  cvmlift2lem10  29814  cvmlift2lem12  29816  cvmlift3lem7  29827  mrsubff1  29931  msubff1  29973  poseq  30269  ifscgr  30587  cgrxfr  30598  btwnconn1lem13  30642  btwnconn1lem14  30643  outsideofeq  30673  ellines  30695  finminlem  30750  fnejoin2  30801  poimirlem13  31647  poimirlem14  31648  poimirlem32  31666  opnmbllem0  31670  mblfinlem3  31673  itg2addnclem  31687  itg2addnc  31690  ftc1cnnc  31710  upixp  31750  filbcmb  31761  sstotbnd2  31800  isbnd3  31810  prdsbnd2  31821  cntotbnd  31822  ismtyima  31829  bfp  31850  rrncmslem  31858  unichnidl  31958  lshpcmp  32253  islshpat  32282  lfl0f  32334  ishlat3N  32619  3dim1  32731  islvol5  32843  lvoli2  32845  lncvrelatN  33045  pclfinclN  33214  pexmidlem8N  33241  idltrn  33414  cdleme42keg  33752  cdleme42mgN  33754  cdlemf2  33828  cdlemg2cex  33857  trlcoat  33989  dihopelvalcpre  34515  dih1dimatlem  34596  dihjatcclem4  34688  lcfl7N  34768  lcfrlem9  34817  mapdh9a  35057  hdmapglem7  35199  nacsfix  35253  mzpsubst  35289  mzpcompact2lem  35292  eldioph2lem2  35302  eldioph2  35303  eldioph2b  35304  diophin  35314  diophun  35315  irrapxlem3  35368  irrapxlem5  35370  pell1234qrreccl  35398  pell1234qrmulcl  35399  pell14qrdich  35413  pell1qrge1  35414  pell1qrgaplem  35417  monotuz  35485  rpexpmord  35492  acongtr  35524  acongrep  35526  jm2.23  35547  jm2.26a  35551  jm2.26lem3  35552  jm2.26  35553  jm2.27  35559  wepwsolem  35596  fnwe2lem2  35605  kelac1  35617  kercvrlsm  35637  hbtlem5  35683  hbt  35685  mpaaeu  35705  cncmpmax  36983  rfcnnnub  36987  iccintsng  37199  lptioo2  37273  lptioo1  37274  limclner  37294  stoweidlem31  37451  stoweidlem34  37454  stoweidlem35  37455  stoweidlem49  37469  stoweidlem59  37479  stoweidlem62  37482  stoweidlem62OLD  37483  fourierdlem60  37588  fourierdlem61  37589  fourierdlem87  37615  iundjiun  37797  ismeannd  37804  perfectALTVlem2  38224  bgoldbtbndlem2  38281  bgoldbtbndlem3  38282  reuccatpfxs1  38355  usgedgvadf1lem2  38474  usgedgvadf1ALTlem2  38477  mgmhmeql  38551  mndpsuppss  38906  scmsuppss  38907  lindslinindsimp2lem5  39005  elfzolborelfzop1  39067  elbigolo1  39119
  Copyright terms: Public domain W3C validator