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

Theorem simplrr 760
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  2769  rmob  3384  disjxiun  4387  isotr  6126  weniso  6144  riota5f  6176  tfrlem9a  6945  oaass  7100  oeeui  7141  oaabs2  7184  resixpfo  7401  omxpenlem  7512  pw2f1olem  7515  fopwdom  7519  fofinf1o  7693  marypha1lem  7784  ordiso2  7830  oismo  7855  ixpiunwdom  7907  cantnf  8002  cantnfOLD  8024  fseqenlem1  8295  iunfictbso  8385  dfac12lem2  8414  dfac12lem3  8415  infunsdom1  8483  infpssrlem5  8577  fin23lem24  8592  isf32lem2  8624  isf32lem4  8626  isf34lem4  8647  fin1a2lem12  8681  fin1a2lem13  8682  ttukeylem6  8784  fpwwe2lem12  8909  fpwwe2lem13  8910  fpwwe2  8911  winalim2  8964  wunex2  9006  tskord  9048  prlem934  9303  dedekind  9634  addid1  9650  cnegex  9651  negeu  9701  add20  9952  divdivdiv  10133  ltmul12a  10286  lemul12a  10288  lediv12a  10326  supmul1  10396  cru  10415  uzwo3  11049  xleadd1a  11317  xmullem  11328  xmulgt0  11347  xlemul1a  11352  ixxun  11417  ixxss12  11421  ioodisj  11516  fz0fzelfz0  11587  mulexpz  12005  leexp1a  12023  expmulnbnd  12097  hashf1  12312  brfi1uzind  12321  abs3lem  12928  rexanre  12936  cau3lem  12944  limsupgre  13061  limsupbnd2  13063  o1lo1  13117  rlimclim1  13125  rlimclim  13126  rlimcn1  13168  rlimcn2  13170  o1of2  13192  o1rlimmul  13198  lo1add  13206  lo1mul  13207  isercolllem1  13244  climcau  13250  caucvgrlem  13252  caucvgb  13259  summolem2  13295  summo  13296  o1fsum  13378  isprm6  13897  isprm5  13900  rpdvds  13912  pclem  14007  pcqmul  14022  pcexp  14028  pcneg  14042  pcprmpw2  14050  pcadd  14053  pcmpt  14056  4sqlem13  14120  vdwlem2  14145  vdwlem7  14150  vdwlem12  14155  ramval  14171  ramub2  14177  ramz2  14187  ramcl  14192  cshwshashlem2  14225  imasval  14551  imasdsval  14555  mreexexd  14688  acsfn  14699  issubc3  14861  idfucl  14893  funcres2c  14913  isnat  14959  fucpropd  14989  xpcval  15089  xpcco  15095  prfval  15111  evlf2  15130  evlfcl  15134  curf12  15139  curf1cl  15140  curf2  15141  curfcl  15144  curf2ndf  15159  hof2val  15168  hofcl  15171  hofpropd  15179  yonedalem4a  15187  yonedainv  15193  drsdirfi  15210  pospo  15245  poslubmo  15418  posglbmo  15419  isipodrs  15433  acsinfd  15452  mndpropd  15548  mhmeql  15594  mrcmndind  15596  gsumvalx  15604  gsumpropd2lem  15607  frmdup3  15646  issubg4  15802  ssnmz  15825  conjnmzb  15883  f1otrspeq  16055  psgneu  16114  pgpfi  16208  sylow2blem3  16225  slwhash  16227  fislw  16228  sylow3lem2  16231  lsmdisj2  16283  pj1eu  16297  efgredlem  16348  frgpuplem  16373  gexex  16439  frgpnabl  16457  dprdfadd  16615  dprdfaddOLD  16622  dpjidcl  16662  dpjidclOLD  16669  pgpfac1lem3  16683  pgpfaclem3  16689  ablfac2  16695  rngpropd  16782  islmhm2  17225  lmhmpropd  17260  lbsextlem4  17348  assapropd  17504  psrval  17535  evlslem1  17708  prmirredlem  18026  prmirredlemOLD  18029  psgndiflemA  18140  lsmcss  18226  uvcf1  18326  frlmsslsp  18332  frlmsslspOLD  18333  frlmup1  18335  mamucl  18410  mamulid  18413  mamurid  18414  mamuass  18415  mamudi  18416  mamudir  18417  mamuvs1  18418  mamuvs2  18419  marrepval  18484  marepveval  18490  mdetunilem7  18540  gsummatr01lem4  18580  pptbas  18728  toponmre  18813  restbas  18878  iscncl  18989  cnrest2  19006  cnpdis  19013  lmcnp  19024  dishaus  19102  cmpcovf  19110  tgcmp  19120  dfcon2  19139  clscon  19150  2ndcctbss  19175  dis2ndc  19180  1stccnp  19182  islly2  19204  cldllycmp  19215  kgentopon  19227  txcls  19293  ptpjopn  19301  dfac14  19307  xkoccn  19308  txcnp  19309  txcmpb  19333  txlm  19337  xkopt  19344  xkoco1cn  19346  xkoco2cn  19347  qtopcn  19403  qtoprest  19406  regr1lem2  19429  xkocnv  19503  qtophmeo  19506  fmfnfmlem4  19646  hausflim  19670  hauspwpwf1  19676  fclscmp  19719  alexsublem  19732  alexsubALTlem2  19736  alexsubALTlem3  19737  ptcmplem3  19742  ptcmplem4  19743  ptcmplem5  19744  cnextfun  19752  tmdgsum2  19783  symgtgp  19788  tsmsval2  19816  tsmsgsum  19825  tsmsgsumOLD  19828  utoptop  19925  ismet2  20024  blin  20112  metss2lem  20202  methaus  20211  met1stc  20212  met2ndci  20213  prdsxmslem2  20220  metcnp3  20231  metcnpi3  20237  metusttoOLD  20248  metustto  20249  metustfbasOLD  20256  metustfbas  20257  nlmvscn  20384  nrginvrcn  20388  xrsxmet  20502  reconnlem1  20519  reconn  20521  xrge0tsms  20527  xmetdcn2  20530  metdscn  20548  addcnlem  20556  fsumcn  20562  cnheiborlem  20642  cnheibor  20643  bndth  20646  lebnum  20652  nmoleub2lem2  20787  ipcn  20874  iscmet3  20920  caubl  20934  rrxdstprj1  21024  minveclem3b  21031  minveclem7  21038  pjthlem2  21041  pmltpc  21050  volfiniun  21144  ioombl1  21159  dyadss  21190  dyaddisjlem  21191  dyadmax  21194  dyadmbllem  21195  opnmbllem  21197  itg1addlem2  21291  itg10a  21304  mbfi1fseqlem6  21314  itg2seq  21336  itg2monolem1  21344  itg2gt0  21354  itgfsum  21420  limcfval  21463  ellimc2  21468  ellimc3  21470  limcres  21477  limciun  21485  dvres  21502  dveflem  21567  rolle  21578  dvlip2  21583  c1liplem1  21584  dvgt0lem1  21590  dvgt0  21592  dvlt0  21593  dvne0  21599  dvfsumrlimge0  21618  ftc1lem6  21629  itgsubst  21637  mdegmullem  21665  ply1domn  21711  ply1divex  21724  fta1g  21755  fta1b  21757  plyf  21782  dgrlem  21813  coeid  21822  plydivalg  21881  aannenlem1  21910  aalioulem3  21916  aalioulem6  21919  abelthlem8  22020  efif1olem4  22117  chordthm  22348  xrlimcnp  22478  jensen  22498  sqf11  22593  fsumvma2  22669  perfectlem2  22685  lgsdilem  22777  lgsquad2lem2  22814  lgsquad3  22816  2sqlem5  22823  2sqlem9  22828  2sqb  22833  rpvmasumlem  22852  dchrisum0flb  22875  dchrisum0  22885  pntpbnd  22953  pntibndlem3  22957  pntleml  22976  legov  23137  legtrid  23143  tglinethru  23164  tglnpt2  23168  tglineintmo  23169  mirreu3  23184  perpcom  23232  colperplem3  23242  mideulem  23244  mideu  23245  brcgr  23281  brbtwn2  23286  colinearalg  23291  axsegcon  23308  axeuclidlem  23343  axcontlem9  23353  ecgrtg  23364  elntg  23365  eengtrkg  23366  cusgrarn  23502  usgrasscusgra  23526  4cycl4dv4e  23689  eupath2  23736  vacn  24224  blocni  24340  ubthlem3  24408  minvecolem7  24419  chocunii  24839  pjhthmo  24840  pjhthlem2  24930  kbass5  25659  mdsymlem5  25946  fcobij  26159  xrofsup  26189  archirngz  26340  archiabllem2a  26345  xrge0tsmsd  26387  isarchiofld  26419  qqhval2  26545  volmeas  26781  ballotlemfc0  27009  ballotlemfcc  27010  signstfvneq0  27107  lgamcvglem  27160  lgamcvg2  27175  derangenlem  27193  erdsze2lem1  27225  pconcon  27254  conpcon  27258  cvxscon  27266  cvmliftmolem2  27305  cvmliftmo  27307  cvmlift2lem10  27335  cvmlift2lem12  27337  cvmlift3lem7  27348  prodmolem2  27582  poseq  27848  ifscgr  28209  cgrxfr  28220  btwnconn1lem13  28264  btwnconn1lem14  28265  outsideofeq  28295  ellines  28317  supaddc  28555  opnmbllem0  28565  mblfinlem3  28568  itg2addnclem  28581  itg2addnc  28584  ftc1cnnc  28604  finminlem  28651  locfincmp  28714  comppfsc  28717  fnejoin2  28728  upixp  28761  filbcmb  28772  sstotbnd2  28811  isbnd3  28821  prdsbnd2  28832  cntotbnd  28833  ismtyima  28840  bfp  28861  rrncmslem  28869  unichnidl  28969  nacsfix  29186  mzpsubst  29223  mzpcompact2lem  29226  eldioph2lem2  29237  eldioph2  29238  eldioph2b  29239  diophin  29249  diophun  29250  irrapxlem3  29303  irrapxlem5  29305  pell1234qrreccl  29333  pell1234qrmulcl  29334  pell14qrdich  29348  pell1qrge1  29349  pell1qrgaplem  29352  monotuz  29420  rpexpmord  29427  acongtr  29459  acongrep  29461  jm2.23  29483  jm2.26a  29487  jm2.26lem3  29488  jm2.26  29489  jm2.27  29495  wepwsolem  29532  fnwe2lem2  29542  kelac1  29554  kercvrlsm  29574  hbtlem5  29622  hbt  29624  mpaaeu  29645  cncmpmax  29892  rfcnnnub  29896  stoweidlem31  29964  stoweidlem34  29967  stoweidlem35  29968  stoweidlem49  29982  stoweidlem59  29992  stoweidlem62  29995  modfsummod  30383  reuccats1  30399  usg2spthonot1  30547  wwlkext2clwwlk  30603  usgfidegfi  30665  usg2spot2nb  30796  numclwwlk6  30844  mndpsuppss  30922  scmsuppss  30923  dmatsubcl  31031  dmatmulcl  31033  scmatmulcl  31040  lindslinindsimp2lem5  31103  cpmatmcllem  31181  mat2pmatf1  31192  mat2pmatlin  31198  pmatcollpw1  31232  pmattomply1mhmlem2  31274  cpidmat  31301  lshpcmp  32939  islshpat  32968  lfl0f  33020  ishlat3N  33305  3dim1  33417  islvol5  33529  lvoli2  33531  lncvrelatN  33731  pclfinclN  33900  pexmidlem8N  33927  idltrn  34100  cdleme42keg  34436  cdleme42mgN  34438  cdlemf2  34512  cdlemg2cex  34541  trlcoat  34673  dihopelvalcpre  35199  dih1dimatlem  35280  dihjatcclem4  35372  lcfl7N  35452  lcfrlem9  35501  mapdh9a  35741  hdmapglem7  35883
  Copyright terms: Public domain W3C validator