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

Theorem simplrr 753
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 458 . 2  |-  ( ( ps  /\  ch )  ->  ch )
21ad2antlr 719 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.61da3ne  2681  rmob  3274  disjxiun  4277  isotr  6014  weniso  6032  riota5f  6065  tfrlem9a  6831  oaass  6988  oeeui  7029  oaabs2  7072  resixpfo  7289  omxpenlem  7400  pw2f1olem  7403  fopwdom  7407  fofinf1o  7580  marypha1lem  7671  ordiso2  7717  oismo  7742  ixpiunwdom  7794  cantnf  7889  cantnfOLD  7911  fseqenlem1  8182  iunfictbso  8272  dfac12lem2  8301  dfac12lem3  8302  infunsdom1  8370  infpssrlem5  8464  fin23lem24  8479  isf32lem2  8511  isf32lem4  8513  isf34lem4  8534  fin1a2lem12  8568  fin1a2lem13  8569  ttukeylem6  8671  fpwwe2lem12  8796  fpwwe2lem13  8797  fpwwe2  8798  winalim2  8851  wunex2  8893  tskord  8935  prlem934  9190  dedekind  9521  addid1  9537  cnegex  9538  negeu  9588  add20  9839  divdivdiv  10020  ltmul12a  10173  lemul12a  10175  lediv12a  10213  supmul1  10283  cru  10302  uzwo3  10936  xleadd1a  11204  xmullem  11215  xmulgt0  11234  xlemul1a  11239  ixxun  11304  ixxss12  11308  ioodisj  11402  fz0fzelfz0  11473  mulexpz  11888  leexp1a  11906  expmulnbnd  11980  hashf1  12194  brfi1uzind  12203  abs3lem  12810  rexanre  12818  cau3lem  12826  limsupgre  12943  limsupbnd2  12945  o1lo1  12999  rlimclim1  13007  rlimclim  13008  rlimcn1  13050  rlimcn2  13052  o1of2  13074  o1rlimmul  13080  lo1add  13088  lo1mul  13089  isercolllem1  13126  climcau  13132  caucvgrlem  13134  caucvgb  13141  summolem2  13177  summo  13178  o1fsum  13259  isprm6  13778  isprm5  13781  rpdvds  13793  pclem  13888  pcqmul  13903  pcexp  13909  pcneg  13923  pcprmpw2  13931  pcadd  13934  pcmpt  13937  4sqlem13  14001  vdwlem2  14026  vdwlem7  14031  vdwlem12  14036  ramval  14052  ramub2  14058  ramz2  14068  ramcl  14073  cshwshashlem2  14106  imasval  14432  imasdsval  14436  mreexexd  14569  acsfn  14580  issubc3  14742  idfucl  14774  funcres2c  14794  isnat  14840  fucpropd  14870  xpcval  14970  xpcco  14976  prfval  14992  evlf2  15011  evlfcl  15015  curf12  15020  curf1cl  15021  curf2  15022  curfcl  15025  curf2ndf  15040  hof2val  15049  hofcl  15052  hofpropd  15060  yonedalem4a  15068  yonedainv  15074  drsdirfi  15091  pospo  15126  poslubmo  15299  posglbmo  15300  isipodrs  15314  acsinfd  15333  mndpropd  15429  mhmeql  15474  mrcmndind  15476  gsumvalx  15484  frmdup3  15524  issubg4  15680  ssnmz  15703  conjnmzb  15761  f1otrspeq  15933  psgneu  15992  pgpfi  16084  sylow2blem3  16101  slwhash  16103  fislw  16104  sylow3lem2  16107  lsmdisj2  16159  pj1eu  16173  efgredlem  16224  frgpuplem  16249  gexex  16315  frgpnabl  16333  dprdfadd  16484  dprdfaddOLD  16491  dpjidcl  16531  dpjidclOLD  16538  pgpfac1lem3  16552  pgpfaclem3  16558  ablfac2  16564  rngpropd  16612  islmhm2  17041  lmhmpropd  17076  lbsextlem4  17164  assapropd  17320  psrval  17363  prmirredlem  17759  prmirredlemOLD  17762  psgndiflemA  17873  lsmcss  17959  uvcf1  18059  frlmsslsp  18065  frlmsslspOLD  18066  frlmup1  18068  mamucl  18143  mamulid  18146  mamurid  18147  mamuass  18148  mamudi  18149  mamudir  18150  mamuvs1  18151  mamuvs2  18152  marrepval  18215  marepveval  18221  mdetunilem7  18266  gsummatr01lem4  18306  pptbas  18454  toponmre  18539  restbas  18604  iscncl  18715  cnrest2  18732  cnpdis  18739  lmcnp  18750  dishaus  18828  cmpcovf  18836  tgcmp  18846  dfcon2  18865  clscon  18876  2ndcctbss  18901  dis2ndc  18906  1stccnp  18908  islly2  18930  cldllycmp  18941  kgentopon  18953  txcls  19019  ptpjopn  19027  dfac14  19033  xkoccn  19034  txcnp  19035  txcmpb  19059  txlm  19063  xkopt  19070  xkoco1cn  19072  xkoco2cn  19073  qtopcn  19129  qtoprest  19132  regr1lem2  19155  xkocnv  19229  qtophmeo  19232  fmfnfmlem4  19372  hausflim  19396  hauspwpwf1  19402  fclscmp  19445  alexsublem  19458  alexsubALTlem2  19462  alexsubALTlem3  19463  ptcmplem3  19468  ptcmplem4  19469  ptcmplem5  19470  cnextfun  19478  tmdgsum2  19509  symgtgp  19514  tsmsval2  19542  tsmsgsum  19551  tsmsgsumOLD  19554  utoptop  19651  ismet2  19750  blin  19838  metss2lem  19928  methaus  19937  met1stc  19938  met2ndci  19939  prdsxmslem2  19946  metcnp3  19957  metcnpi3  19963  metusttoOLD  19974  metustto  19975  metustfbasOLD  19982  metustfbas  19983  nlmvscn  20110  nrginvrcn  20114  xrsxmet  20228  reconnlem1  20245  reconn  20247  xrge0tsms  20253  xmetdcn2  20256  metdscn  20274  addcnlem  20282  fsumcn  20288  cnheiborlem  20368  cnheibor  20369  bndth  20372  lebnum  20378  nmoleub2lem2  20513  ipcn  20600  iscmet3  20646  caubl  20660  rrxdstprj1  20750  minveclem3b  20757  minveclem7  20764  pjthlem2  20767  pmltpc  20776  volfiniun  20870  ioombl1  20885  dyadss  20916  dyaddisjlem  20917  dyadmax  20920  dyadmbllem  20921  opnmbllem  20923  itg1addlem2  21017  itg10a  21030  mbfi1fseqlem6  21040  itg2seq  21062  itg2monolem1  21070  itg2gt0  21080  itgfsum  21146  limcfval  21189  ellimc2  21194  ellimc3  21196  limcres  21203  limciun  21211  dvres  21228  dveflem  21293  rolle  21304  dvlip2  21309  c1liplem1  21310  dvgt0lem1  21316  dvgt0  21318  dvlt0  21319  dvne0  21325  dvfsumrlimge0  21344  ftc1lem6  21355  itgsubst  21363  evlslem1  21367  mdegmullem  21434  ply1domn  21480  ply1divex  21493  fta1g  21524  fta1b  21526  plyf  21551  dgrlem  21582  coeid  21591  plydivalg  21650  aannenlem1  21679  aalioulem3  21685  aalioulem6  21688  abelthlem8  21789  efif1olem4  21886  chordthm  22117  xrlimcnp  22247  jensen  22267  sqf11  22362  fsumvma2  22438  perfectlem2  22454  lgsdilem  22546  lgsquad2lem2  22583  lgsquad3  22585  2sqlem5  22592  2sqlem9  22597  2sqb  22602  rpvmasumlem  22621  dchrisum0flb  22644  dchrisum0  22654  pntpbnd  22722  pntibndlem3  22726  pntleml  22745  legov  22892  legtrid  22898  tglinethru  22913  tglineintmo  22917  mirreu3  22924  brcgr  22969  brbtwn2  22974  colinearalg  22979  axsegcon  22996  axeuclidlem  23031  axcontlem9  23041  ecgrtg  23052  elntg  23053  eengtrkg  23054  cusgrarn  23190  usgrasscusgra  23214  4cycl4dv4e  23377  eupath2  23424  vacn  23912  blocni  24028  ubthlem3  24096  minvecolem7  24107  chocunii  24527  pjhthmo  24528  pjhthlem2  24618  kbass5  25347  mdsymlem5  25634  fcobij  25849  xrofsup  25878  archirngz  26030  archiabllem2a  26035  gsumpropd2lem  26093  xrge0tsmsd  26106  isarchiofld  26138  qqhval2  26265  volmeas  26501  ballotlemfc0  26723  ballotlemfcc  26724  signstfvneq0  26821  lgamcvglem  26874  lgamcvg2  26889  derangenlem  26907  erdsze2lem1  26939  pconcon  26968  conpcon  26972  cvxscon  26980  cvmliftmolem2  27019  cvmliftmo  27021  cvmlift2lem10  27049  cvmlift2lem12  27051  cvmlift3lem7  27062  prodmolem2  27295  poseq  27561  ifscgr  27922  cgrxfr  27933  btwnconn1lem13  27977  btwnconn1lem14  27978  outsideofeq  28008  ellines  28030  supaddc  28261  opnmbllem0  28271  mblfinlem3  28274  itg2addnclem  28287  itg2addnc  28290  ftc1cnnc  28310  finminlem  28357  locfincmp  28420  comppfsc  28423  fnejoin2  28434  upixp  28467  filbcmb  28478  sstotbnd2  28517  isbnd3  28527  prdsbnd2  28538  cntotbnd  28539  ismtyima  28546  bfp  28567  rrncmslem  28575  unichnidl  28675  nacsfix  28893  mzpsubst  28930  mzpcompact2lem  28933  eldioph2lem2  28944  eldioph2  28945  eldioph2b  28946  diophin  28956  diophun  28957  irrapxlem3  29010  irrapxlem5  29012  pell1234qrreccl  29040  pell1234qrmulcl  29041  pell14qrdich  29055  pell1qrge1  29056  pell1qrgaplem  29059  monotuz  29127  rpexpmord  29134  acongtr  29166  acongrep  29168  jm2.23  29190  jm2.26a  29194  jm2.26lem3  29195  jm2.26  29196  jm2.27  29202  wepwsolem  29239  fnwe2lem2  29249  kelac1  29261  kercvrlsm  29281  hbtlem5  29329  hbt  29331  mpaaeu  29352  cncmpmax  29599  rfcnnnub  29603  stoweidlem31  29672  stoweidlem34  29675  stoweidlem35  29676  stoweidlem49  29690  stoweidlem59  29700  stoweidlem62  29703  modfsummod  30091  reuccats1  30107  usg2spthonot1  30255  wwlkext2clwwlk  30311  usgfidegfi  30373  usg2spot2nb  30504  numclwwlk6  30552  mndpsuppss  30615  scmsuppss  30616  lindslinindsimp2lem5  30705  lshpcmp  32206  islshpat  32235  lfl0f  32287  ishlat3N  32572  3dim1  32684  islvol5  32796  lvoli2  32798  lncvrelatN  32998  pclfinclN  33167  pexmidlem8N  33194  idltrn  33367  cdleme42keg  33703  cdleme42mgN  33705  cdlemf2  33779  cdlemg2cex  33808  trlcoat  33940  dihopelvalcpre  34466  dih1dimatlem  34547  dihjatcclem4  34639  lcfl7N  34719  lcfrlem9  34768  mapdh9a  35008  hdmapglem7  35150
  Copyright terms: Public domain W3C validator