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

Theorem simplrr 776
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 467 . 2  |-  ( ( ps  /\  ch )  ->  ch )
21ad2antlr 738 1  |-  ( ( ( ph  /\  ( ps  /\  ch ) )  /\  th )  ->  ch )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 375
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 190  df-an 377
This theorem is referenced by:  rmob  3371  disjxiun  4413  fsnex  6206  f1prex  6207  isotr  6252  weniso  6270  riota5f  6301  tfrlem9a  7130  oaass  7288  oeeui  7329  oaabs2  7372  resixpfo  7586  omxpenlem  7699  pw2f1olem  7702  fopwdom  7706  fofinf1o  7878  marypha1lem  7973  ordiso2  8056  oismo  8081  ixpiunwdom  8132  cantnf  8224  fseqenlem1  8481  iunfictbso  8571  dfac12lem2  8600  dfac12lem3  8601  infunsdom1  8669  infpssrlem5  8763  fin23lem24  8778  isf32lem2  8810  isf32lem4  8812  isf34lem4  8833  fin1a2lem12  8867  fin1a2lem13  8868  ttukeylem6  8970  fpwwe2lem12  9092  fpwwe2lem13  9093  fpwwe2  9094  winalim2  9147  wunex2  9189  tskord  9231  prlem934  9484  mulcmpblnr  9521  dedekind  9823  addid1  9839  cnegex  9840  negeu  9891  add20  10154  divdivdiv  10336  ltmul12a  10489  lemul12a  10491  lediv12a  10527  supaddc  10602  supmul1  10604  cru  10629  uzwo3  11288  xleadd1a  11568  xmullem  11579  xmulgt0  11598  xlemul1a  11603  ixxun  11680  ixxss12  11684  ioodisj  11791  fz0fzelfz0  11926  mulexpz  12344  leexp1a  12363  expmulnbnd  12436  hashf1  12653  fi1uzind  12683  brfi1indALT  12686  reuccats1  12874  abs3lem  13450  rexanre  13458  cau3lem  13466  limsupgre  13591  limsupgreOLD  13592  limsupbnd2  13595  limsupbnd2OLD  13596  o1lo1  13650  rlimclim1  13658  rlimclim  13659  rlimcn1  13701  rlimcn2  13703  o1of2  13725  o1rlimmul  13731  lo1add  13739  lo1mul  13740  isercolllem1  13777  climcau  13783  caucvgrlem  13785  caucvgrlemOLD  13786  caucvgb  13795  summolem2  13831  summo  13832  modfsummod  13903  o1fsum  13922  prodmolem2  14038  isprm5  14700  isprm6  14715  rpdvds  14725  pclem  14837  pcqmul  14852  pcexp  14858  pcneg  14872  pcprmpw2  14880  pcadd  14883  pcmpt  14886  4sqlem13OLD  14950  4sqlem13  14956  vdwlem2  14981  vdwlem7  14986  vdwlem12  14991  ramval  15009  ramvalOLD  15010  ramub2  15020  ramz2  15031  ramcl  15036  cshwshashlem2  15116  imasval  15460  imasvalOLD  15461  imasdsval  15465  imasdsvalOLD  15477  mreexexd  15603  acsfn  15614  issubc3  15803  idfucl  15835  funcres2c  15855  isnat  15901  fucpropd  15931  xpcval  16111  xpcco  16117  prfval  16133  evlf2  16152  evlfcl  16156  curf12  16161  curf1cl  16162  curf2  16163  curfcl  16166  curf2ndf  16181  hof2val  16190  hofcl  16193  hofpropd  16201  yonedalem4a  16209  yonedainv  16215  drsdirfi  16232  pospo  16268  poslubmo  16441  posglbmo  16442  isipodrs  16456  acsinfd  16475  gsumvalx  16562  gsumpropd2lem  16565  ismndd  16608  mndpropd  16611  mhmeql  16660  mrcmndind  16662  frmdup3lem  16699  mhmmnd  16857  issubg4  16885  ssnmz  16908  conjnmzb  16966  f1otrspeq  17137  psgneu  17196  pgpfi  17306  sylow2blem3  17323  slwhash  17325  fislw  17326  sylow3lem2  17329  lsmdisj2  17381  pj1eu  17395  efgredlem  17446  frgpuplem  17471  gexex  17540  frgpnabl  17560  dprdfadd  17702  dpjidcl  17740  pgpfac1lem3  17759  pgpfaclem3  17765  ablfac2  17771  ringpropd  17861  islmhm2  18310  lmhmpropd  18345  lbsextlem4  18433  assapropd  18600  psrval  18635  evlslem1  18787  prmirredlem  19113  psgndiflemA  19218  lsmcss  19304  uvcf1  19399  frlmsslsp  19403  frlmup1  19405  mamucl  19475  mamuass  19476  mamudi  19477  mamudir  19478  mamuvs1  19479  mamuvs2  19480  mamulid  19515  mamurid  19516  dmatsubcl  19572  dmatmulcl  19574  scmatscm  19587  marrepval  19636  marepveval  19642  mdetunilem7  19692  gsummatr01lem4  19732  cpmatmcllem  19791  mat2pmatf1  19802  mat2pmatlin  19808  decpmatmul  19845  pm2mpmhmlem2  19892  chpidmat  19920  pptbas  20072  toponmre  20158  restbas  20223  iscncl  20334  cnrest2  20351  cnpdis  20358  lmcnp  20369  dishaus  20447  cmpcovf  20455  tgcmp  20465  dfcon2  20483  clscon  20494  2ndcctbss  20519  dis2ndc  20524  1stccnp  20526  islly2  20548  cldllycmp  20559  locfincmp  20590  comppfsc  20596  kgentopon  20602  txcls  20668  ptpjopn  20676  dfac14  20682  xkoccn  20683  txcnp  20684  txcmpb  20708  txlm  20712  xkopt  20719  xkoco1cn  20721  xkoco2cn  20722  qtopcn  20778  qtoprest  20781  regr1lem2  20804  xkocnv  20878  qtophmeo  20881  fmfnfmlem4  21021  hausflim  21045  hauspwpwf1  21051  fclscmp  21094  alexsublem  21108  alexsubALTlem2  21112  alexsubALTlem3  21113  ptcmplem3  21118  ptcmplem4  21119  ptcmplem5  21120  cnextfun  21128  tmdgsum2  21160  symgtgp  21165  tsmsval2  21193  tsmsgsum  21202  utoptop  21298  ismet2  21397  blin  21485  metss2lem  21575  methaus  21584  met1stc  21585  met2ndci  21586  prdsxmslem2  21593  metcnp3  21604  metcnpi3  21610  metustto  21617  metustfbas  21621  nlmvscn  21739  nrginvrcn  21743  xrsxmet  21876  reconnlem1  21893  reconn  21895  xrge0tsms  21901  xmetdcn2  21904  metdscn  21922  metdscnOLD  21937  addcnlem  21945  fsumcn  21951  cnheiborlem  22031  cnheibor  22032  bndth  22035  lebnum  22044  nmoleub2lem2  22179  ipcn  22266  iscmet3  22312  caubl  22326  rrxdstprj1  22412  minveclem3b  22419  minveclem7  22426  minveclem3bOLD  22431  minveclem7OLD  22438  pjthlem2  22441  pmltpc  22450  volfiniun  22549  ioombl1  22564  dyadss  22601  dyaddisjlem  22602  dyadmax  22605  dyadmbllem  22606  opnmbllem  22608  itg1addlem2  22704  itg10a  22717  mbfi1fseqlem6  22727  itg2seq  22749  itg2monolem1  22757  itg2gt0  22767  itgfsum  22833  limcfval  22876  ellimc2  22881  ellimc3  22883  limcres  22890  limciun  22898  dvres  22915  dveflem  22980  rolle  22991  dvlip2  22996  c1liplem1  22997  dvgt0lem1  23003  dvgt0  23005  dvlt0  23006  dvne0  23012  dvfsumrlimge0  23031  ftc1lem6  23042  itgsubst  23050  mdegmullem  23076  ply1domn  23121  ply1divex  23136  fta1g  23167  fta1b  23169  plyf  23201  dgrlem  23232  coeid  23241  plydivalg  23301  aannenlem1  23333  aalioulem3  23339  aalioulem6  23342  abelthlem8  23443  efif1olem4  23543  chordthm  23812  xrlimcnp  23943  jensen  23963  lgamcvglem  24014  lgamcvg2  24029  sqf11  24115  fsumvma2  24191  perfectlem2  24207  lgsdilem  24299  lgsquad2lem2  24336  lgsquad3  24338  2sqlem5  24345  2sqlem9  24350  2sqb  24355  rpvmasumlem  24374  dchrisum0flb  24397  dchrisum0  24407  pntpbnd  24475  pntibndlem3  24479  pntleml  24498  legov  24679  legtrid  24685  tglinethru  24730  tglnpt2  24735  tglineintmo  24736  mirreu3  24748  perpcom  24807  colperpexlem3  24823  mideu  24829  opphllem1  24838  hlpasch  24847  lnopp2hpgb  24854  trgcopy  24895  brcgr  24979  brbtwn2  24984  colinearalg  24989  axsegcon  25006  axeuclidlem  25041  axcontlem9  25051  ecgrtg  25062  elntg  25063  eengtrkg  25064  cusgrarn  25236  usgrasscusgra  25260  4cycl4dv4e  25445  wwlkext2clwwlk  25580  usg2spthonot1  25667  usgfidegfi  25687  eupath2  25757  usg2spot2nb  25842  numclwwlk6  25890  vacn  26379  blocni  26495  ubthlem3  26563  minvecolem7  26574  minvecolem7OLD  26584  chocunii  27003  pjhthmo  27004  pjhthlem2  27094  kbass5  27822  mdsymlem5  28109  foresf1o  28188  fcobij  28359  xrofsup  28402  archirngz  28555  archiabllem2a  28560  xrge0tsmsd  28597  isarchiofld  28629  smatrcl  28671  reff  28715  ordtconlem1  28779  qqhval2  28835  volmeas  29103  fiunelcarsg  29197  ballotlemfc0  29374  ballotlemfcc  29375  signstfvneq0  29510  derangenlem  29943  erdsze2lem1  29975  pconcon  30003  conpcon  30007  cvxscon  30015  cvmliftmolem2  30054  cvmliftmo  30056  cvmlift2lem10  30084  cvmlift2lem12  30086  cvmlift3lem7  30097  mrsubff1  30201  msubff1  30243  poseq  30540  ifscgr  30860  cgrxfr  30871  btwnconn1lem13  30915  btwnconn1lem14  30916  outsideofeq  30946  ellines  30968  finminlem  31023  fnejoin2  31074  poimirlem13  31998  poimirlem14  31999  poimirlem32  32017  opnmbllem0  32021  mblfinlem3  32024  itg2addnclem  32038  itg2addnc  32041  ftc1cnnc  32061  upixp  32101  filbcmb  32112  sstotbnd2  32151  isbnd3  32161  prdsbnd2  32172  cntotbnd  32173  ismtyima  32180  bfp  32201  rrncmslem  32209  unichnidl  32309  lshpcmp  32599  islshpat  32628  lfl0f  32680  ishlat3N  32965  3dim1  33077  islvol5  33189  lvoli2  33191  lncvrelatN  33391  pclfinclN  33560  pexmidlem8N  33587  idltrn  33760  cdleme42keg  34098  cdleme42mgN  34100  cdlemf2  34174  cdlemg2cex  34203  trlcoat  34335  dihopelvalcpre  34861  dih1dimatlem  34942  dihjatcclem4  35034  lcfl7N  35114  lcfrlem9  35163  mapdh9a  35403  hdmapglem7  35545  nacsfix  35599  mzpsubst  35635  mzpcompact2lem  35638  eldioph2lem2  35648  eldioph2  35649  eldioph2b  35650  diophin  35660  diophun  35661  irrapxlem3  35713  irrapxlem5  35715  pell1234qrreccl  35745  pell1234qrmulcl  35746  pell14qrdich  35760  pell1qrge1  35761  pell1qrgaplem  35764  monotuz  35834  rpexpmord  35841  acongtr  35873  acongrep  35875  jm2.23  35896  jm2.26a  35900  jm2.26lem3  35901  jm2.26  35902  jm2.27  35908  wepwsolem  35945  fnwe2lem2  35954  kelac1  35966  kercvrlsm  35986  hbtlem5  36032  hbt  36034  mpaaeu  36061  cncmpmax  37393  rfcnnnub  37397  disjxp1  37449  iccintsng  37662  lptioo2  37749  lptioo1  37750  limclner  37770  stoweidlem31  37930  stoweidlem34  37933  stoweidlem35  37934  stoweidlem49  37948  stoweidlem59  37958  stoweidlem62  37961  stoweidlem62OLD  37962  fourierdlem60  38068  fourierdlem61  38069  fourierdlem87  38095  iundjiun  38336  ismeannd  38343  hoidmvle  38460  perfectALTVlem2  38882  bgoldbtbndlem2  38939  bgoldbtbndlem3  38940  reuccatpfxs1  39015  upgr1eopALT  39253  usgredg4  39344  subuhgr  39408  subumgr  39410  usgedgvadf1lem2  39999  usgedgvadf1ALTlem2  40002  mgmhmeql  40076  mndpsuppss  40429  scmsuppss  40430  lindslinindsimp2lem5  40528  elfzolborelfzop1  40589  elbigolo1  40641
  Copyright terms: Public domain W3C validator