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

Theorem simplrr 762
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 461 . 2  |-  ( ( ps  /\  ch )  ->  ch )
21ad2antlr 726 1  |-  ( ( ( ph  /\  ( ps  /\  ch ) )  /\  th )  ->  ch )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369
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
This theorem is referenced by:  pm2.61da3neOLD  2764  rmob  3416  disjxiun  4434  isotr  6217  weniso  6235  riota5f  6267  tfrlem9a  7057  oaass  7212  oeeui  7253  oaabs2  7296  resixpfo  7509  omxpenlem  7620  pw2f1olem  7623  fopwdom  7627  fofinf1o  7803  marypha1lem  7895  ordiso2  7943  oismo  7968  ixpiunwdom  8020  cantnf  8115  cantnfOLD  8137  fseqenlem1  8408  iunfictbso  8498  dfac12lem2  8527  dfac12lem3  8528  infunsdom1  8596  infpssrlem5  8690  fin23lem24  8705  isf32lem2  8737  isf32lem4  8739  isf34lem4  8760  fin1a2lem12  8794  fin1a2lem13  8795  ttukeylem6  8897  fpwwe2lem12  9022  fpwwe2lem13  9023  fpwwe2  9024  winalim2  9077  wunex2  9119  tskord  9161  prlem934  9414  mulcmpblnr  9451  dedekind  9747  addid1  9763  cnegex  9764  negeu  9815  add20  10071  divdivdiv  10252  ltmul12a  10405  lemul12a  10407  lediv12a  10445  supmul1  10515  cru  10535  uzwo3  11188  xleadd1a  11456  xmullem  11467  xmulgt0  11486  xlemul1a  11491  ixxun  11556  ixxss12  11560  ioodisj  11661  fz0fzelfz0  11791  mulexpz  12188  leexp1a  12206  expmulnbnd  12280  hashf1  12488  brfi1uzind  12514  reuccats1  12688  abs3lem  13153  rexanre  13161  cau3lem  13169  limsupgre  13286  limsupbnd2  13288  o1lo1  13342  rlimclim1  13350  rlimclim  13351  rlimcn1  13393  rlimcn2  13395  o1of2  13417  o1rlimmul  13423  lo1add  13431  lo1mul  13432  isercolllem1  13469  climcau  13475  caucvgrlem  13477  caucvgb  13484  summolem2  13520  summo  13521  modfsummod  13590  o1fsum  13609  prodmolem2  13724  isprm6  14232  isprm5  14235  rpdvds  14247  pclem  14344  pcqmul  14359  pcexp  14365  pcneg  14379  pcprmpw2  14387  pcadd  14390  pcmpt  14393  4sqlem13  14457  vdwlem2  14482  vdwlem7  14487  vdwlem12  14492  ramval  14508  ramub2  14514  ramz2  14524  ramcl  14529  cshwshashlem2  14563  imasval  14890  imasdsval  14894  mreexexd  15027  acsfn  15038  issubc3  15197  idfucl  15229  funcres2c  15249  isnat  15295  fucpropd  15325  xpcval  15425  xpcco  15431  prfval  15447  evlf2  15466  evlfcl  15470  curf12  15475  curf1cl  15476  curf2  15477  curfcl  15480  curf2ndf  15495  hof2val  15504  hofcl  15507  hofpropd  15515  yonedalem4a  15523  yonedainv  15529  drsdirfi  15546  pospo  15582  poslubmo  15755  posglbmo  15756  isipodrs  15770  acsinfd  15789  gsumvalx  15876  gsumpropd2lem  15879  ismndd  15922  mndpropd  15925  mhmeql  15974  mrcmndind  15976  frmdup3lem  16013  mhmmnd  16171  issubg4  16199  ssnmz  16222  conjnmzb  16280  f1otrspeq  16451  psgneu  16510  pgpfi  16604  sylow2blem3  16621  slwhash  16623  fislw  16624  sylow3lem2  16627  lsmdisj2  16679  pj1eu  16693  efgredlem  16744  frgpuplem  16769  gexex  16838  frgpnabl  16858  dprdfadd  17039  dprdfaddOLD  17046  dpjidcl  17086  dpjidclOLD  17093  pgpfac1lem3  17107  pgpfaclem3  17113  ablfac2  17119  ringpropd  17209  islmhm2  17663  lmhmpropd  17698  lbsextlem4  17786  assapropd  17955  psrval  17990  evlslem1  18163  prmirredlem  18501  prmirredlemOLD  18504  psgndiflemA  18615  lsmcss  18701  uvcf1  18801  frlmsslsp  18807  frlmsslspOLD  18808  frlmup1  18810  mamucl  18881  mamuass  18882  mamudi  18883  mamudir  18884  mamuvs1  18885  mamuvs2  18886  mamulid  18921  mamurid  18922  dmatsubcl  18978  dmatmulcl  18980  scmatscm  18993  marrepval  19042  marepveval  19048  mdetunilem7  19098  gsummatr01lem4  19138  cpmatmcllem  19197  mat2pmatf1  19208  mat2pmatlin  19214  decpmatmul  19251  pm2mpmhmlem2  19298  chpidmat  19326  pptbas  19487  toponmre  19572  restbas  19637  iscncl  19748  cnrest2  19765  cnpdis  19772  lmcnp  19783  dishaus  19861  cmpcovf  19869  tgcmp  19879  dfcon2  19898  clscon  19909  2ndcctbss  19934  dis2ndc  19939  1stccnp  19941  islly2  19963  cldllycmp  19974  locfincmp  20005  comppfsc  20011  kgentopon  20017  txcls  20083  ptpjopn  20091  dfac14  20097  xkoccn  20098  txcnp  20099  txcmpb  20123  txlm  20127  xkopt  20134  xkoco1cn  20136  xkoco2cn  20137  qtopcn  20193  qtoprest  20196  regr1lem2  20219  xkocnv  20293  qtophmeo  20296  fmfnfmlem4  20436  hausflim  20460  hauspwpwf1  20466  fclscmp  20509  alexsublem  20522  alexsubALTlem2  20526  alexsubALTlem3  20527  ptcmplem3  20532  ptcmplem4  20533  ptcmplem5  20534  cnextfun  20542  tmdgsum2  20573  symgtgp  20578  tsmsval2  20606  tsmsgsum  20615  tsmsgsumOLD  20618  utoptop  20715  ismet2  20814  blin  20902  metss2lem  20992  methaus  21001  met1stc  21002  met2ndci  21003  prdsxmslem2  21010  metcnp3  21021  metcnpi3  21027  metusttoOLD  21038  metustto  21039  metustfbasOLD  21046  metustfbas  21047  nlmvscn  21174  nrginvrcn  21178  xrsxmet  21292  reconnlem1  21309  reconn  21311  xrge0tsms  21317  xmetdcn2  21320  metdscn  21338  addcnlem  21346  fsumcn  21352  cnheiborlem  21432  cnheibor  21433  bndth  21436  lebnum  21442  nmoleub2lem2  21577  ipcn  21664  iscmet3  21710  caubl  21724  rrxdstprj1  21814  minveclem3b  21821  minveclem7  21828  pjthlem2  21831  pmltpc  21840  volfiniun  21935  ioombl1  21950  dyadss  21981  dyaddisjlem  21982  dyadmax  21985  dyadmbllem  21986  opnmbllem  21988  itg1addlem2  22082  itg10a  22095  mbfi1fseqlem6  22105  itg2seq  22127  itg2monolem1  22135  itg2gt0  22145  itgfsum  22211  limcfval  22254  ellimc2  22259  ellimc3  22261  limcres  22268  limciun  22276  dvres  22293  dveflem  22358  rolle  22369  dvlip2  22374  c1liplem1  22375  dvgt0lem1  22381  dvgt0  22383  dvlt0  22384  dvne0  22390  dvfsumrlimge0  22409  ftc1lem6  22420  itgsubst  22428  mdegmullem  22456  ply1domn  22502  ply1divex  22515  fta1g  22546  fta1b  22548  plyf  22573  dgrlem  22604  coeid  22613  plydivalg  22673  aannenlem1  22702  aalioulem3  22708  aalioulem6  22711  abelthlem8  22812  efif1olem4  22910  chordthm  23146  xrlimcnp  23276  jensen  23296  sqf11  23391  fsumvma2  23467  perfectlem2  23483  lgsdilem  23575  lgsquad2lem2  23612  lgsquad3  23614  2sqlem5  23621  2sqlem9  23626  2sqb  23631  rpvmasumlem  23650  dchrisum0flb  23673  dchrisum0  23683  pntpbnd  23751  pntibndlem3  23755  pntleml  23774  legov  23950  legtrid  23956  tglinethru  23994  tglnpt2  23999  tglineintmo  24000  mirreu3  24013  perpcom  24068  colperpexlem3  24084  mideu  24090  opphllem1  24097  lnopp2hpgb  24110  brcgr  24181  brbtwn2  24186  colinearalg  24191  axsegcon  24208  axeuclidlem  24243  axcontlem9  24253  ecgrtg  24264  elntg  24265  eengtrkg  24266  cusgrarn  24437  usgrasscusgra  24461  4cycl4dv4e  24646  wwlkext2clwwlk  24781  usg2spthonot1  24868  usgfidegfi  24888  eupath2  24958  usg2spot2nb  25043  numclwwlk6  25091  vacn  25582  blocni  25698  ubthlem3  25766  minvecolem7  25777  chocunii  26197  pjhthmo  26198  pjhthlem2  26288  kbass5  27017  mdsymlem5  27304  foresf1o  27381  fcobij  27526  xrofsup  27560  archirngz  27711  archiabllem2a  27716  xrge0tsmsd  27753  isarchiofld  27785  reff  27820  ordtconlem1  27884  qqhval2  27941  volmeas  28181  ballotlemfc0  28409  ballotlemfcc  28410  signstfvneq0  28507  lgamcvglem  28560  lgamcvg2  28575  derangenlem  28593  erdsze2lem1  28625  pconcon  28654  conpcon  28658  cvxscon  28666  cvmliftmolem2  28705  cvmliftmo  28707  cvmlift2lem10  28735  cvmlift2lem12  28737  cvmlift3lem7  28748  mrsubff1  28852  msubff1  28894  poseq  29309  ifscgr  29670  cgrxfr  29681  btwnconn1lem13  29725  btwnconn1lem14  29726  outsideofeq  29756  ellines  29778  supaddc  30017  opnmbllem0  30026  mblfinlem3  30029  itg2addnclem  30042  itg2addnc  30045  ftc1cnnc  30065  finminlem  30112  fnejoin2  30163  upixp  30196  filbcmb  30207  sstotbnd2  30246  isbnd3  30256  prdsbnd2  30267  cntotbnd  30268  ismtyima  30275  bfp  30296  rrncmslem  30304  unichnidl  30404  nacsfix  30620  mzpsubst  30657  mzpcompact2lem  30660  eldioph2lem2  30670  eldioph2  30671  eldioph2b  30672  diophin  30682  diophun  30683  irrapxlem3  30736  irrapxlem5  30738  pell1234qrreccl  30766  pell1234qrmulcl  30767  pell14qrdich  30781  pell1qrge1  30782  pell1qrgaplem  30785  monotuz  30853  rpexpmord  30860  acongtr  30892  acongrep  30894  jm2.23  30914  jm2.26a  30918  jm2.26lem3  30919  jm2.26  30920  jm2.27  30926  wepwsolem  30963  fnwe2lem2  30973  kelac1  30985  kercvrlsm  31005  hbtlem5  31053  hbt  31055  mpaaeu  31075  cncmpmax  31361  rfcnnnub  31365  iccintsng  31517  lptioo2  31591  lptioo1  31592  limclner  31611  stoweidlem31  31767  stoweidlem34  31770  stoweidlem35  31771  stoweidlem49  31785  stoweidlem59  31795  stoweidlem62  31798  fourierdlem60  31903  fourierdlem61  31904  fourierdlem87  31930  usgedgvadf1lem2  32368  usgedgvadf1ALTlem2  32371  mgmhmeql  32445  mndpsuppss  32834  scmsuppss  32835  lindslinindsimp2lem5  32933  lshpcmp  34588  islshpat  34617  lfl0f  34669  ishlat3N  34954  3dim1  35066  islvol5  35178  lvoli2  35180  lncvrelatN  35380  pclfinclN  35549  pexmidlem8N  35576  idltrn  35749  cdleme42keg  36087  cdleme42mgN  36089  cdlemf2  36163  cdlemg2cex  36192  trlcoat  36324  dihopelvalcpre  36850  dih1dimatlem  36931  dihjatcclem4  37023  lcfl7N  37103  lcfrlem9  37152  mapdh9a  37392  hdmapglem7  37534
  Copyright terms: Public domain W3C validator