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

Theorem simplrr 738
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 448 . 2  |-  ( ( ps  /\  ch )  ->  ch )
21ad2antlr 708 1  |-  ( ( ( ph  /\  ( ps  /\  ch ) )  /\  th )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359
This theorem is referenced by:  pm2.61da3ne  2651  rmob  3213  disjxiun  4173  isotr  6019  weniso  6038  riota5f  6537  tfrlem9a  6610  oaass  6767  oeeui  6808  oaabs2  6851  resixpfo  7063  omxpenlem  7172  pw2f1olem  7175  fopwdom  7179  fofinf1o  7350  marypha1lem  7400  ordiso2  7444  oismo  7469  ixpiunwdom  7519  cantnf  7609  fseqenlem1  7865  iunfictbso  7955  dfac12lem2  7984  dfac12lem3  7985  infunsdom1  8053  infpssrlem5  8147  fin23lem24  8162  isf32lem2  8194  isf32lem4  8196  isf34lem4  8217  fin1a2lem12  8251  fin1a2lem13  8252  ttukeylem6  8354  fpwwe2lem12  8476  fpwwe2lem13  8477  fpwwe2  8478  winalim2  8531  wunex2  8573  tskord  8615  prlem934  8870  addid1  9206  cnegex  9207  negeu  9256  add20  9500  divdivdiv  9675  ltmul12a  9826  lemul12a  9828  lediv12a  9863  supmul1  9933  cru  9952  uzwo3  10529  xleadd1a  10792  xmullem  10803  xmulgt0  10822  xlemul1a  10827  ixxun  10892  ixxss12  10896  ioodisj  10986  mulexpz  11379  leexp1a  11397  expmulnbnd  11470  hashf1  11665  brfi1uzind  11674  abs3lem  12101  rexanre  12109  cau3lem  12117  limsupgre  12234  limsupbnd2  12236  o1lo1  12290  rlimclim1  12298  rlimclim  12299  rlimcn1  12341  rlimcn2  12343  o1of2  12365  o1rlimmul  12371  lo1add  12379  lo1mul  12380  isercolllem1  12417  climcau  12423  caucvgrlem  12425  caucvgb  12432  summolem2  12469  summo  12470  o1fsum  12551  isprm6  13068  isprm5  13071  rpdvds  13083  pclem  13171  pcqmul  13186  pcexp  13192  pcneg  13206  pcprmpw2  13214  pcadd  13217  pcmpt  13220  4sqlem13  13284  vdwlem2  13309  vdwlem7  13314  vdwlem12  13319  ramval  13335  ramub2  13341  ramz2  13351  ramcl  13356  imasval  13696  imasdsval  13700  mreexexd  13832  acsfn  13843  issubc3  14005  idfucl  14037  funcres2c  14057  isnat  14103  fucpropd  14133  xpcval  14233  xpcco  14239  prfval  14255  evlf2  14274  evlfcl  14278  curf12  14283  curf1cl  14284  curf2  14285  curfcl  14288  curf2ndf  14303  hof2val  14312  hofcl  14315  hofpropd  14323  yonedalem4a  14331  yonedainv  14337  drsdirfi  14354  pospo  14389  poslubmo  14532  isipodrs  14546  acsinfd  14565  mndpropd  14680  mhmeql  14723  gsumvalx  14733  frmdup3  14770  issubg4  14920  ssnmz  14941  conjnmzb  14999  pgpfi  15198  sylow2blem3  15215  slwhash  15217  fislw  15218  sylow3lem2  15221  lsmdisj2  15273  pj1eu  15287  efgredlem  15338  frgpuplem  15363  gexex  15427  frgpnabl  15445  dprdfadd  15537  dpjidcl  15575  pgpfac1lem3  15594  pgpfaclem3  15600  ablfac2  15606  rngpropd  15654  islmhm2  16073  lmhmpropd  16104  lbsextlem4  16192  assapropd  16345  psrval  16388  prmirredlem  16732  lsmcss  16878  pptbas  17031  toponmre  17116  restbas  17180  iscncl  17291  cnrest2  17308  cnpdis  17315  lmcnp  17326  dishaus  17404  cmpcovf  17412  tgcmp  17422  dfcon2  17439  clscon  17450  2ndcctbss  17475  dis2ndc  17480  1stccnp  17482  islly2  17504  cldllycmp  17515  kgentopon  17527  txcls  17593  ptpjopn  17601  dfac14  17607  xkoccn  17608  txcnp  17609  txcmpb  17633  txlm  17637  xkopt  17644  xkoco1cn  17646  xkoco2cn  17647  qtopcn  17703  qtoprest  17706  regr1lem2  17729  xkocnv  17803  qtophmeo  17806  fmfnfmlem4  17946  hausflim  17970  hauspwpwf1  17976  fclscmp  18019  alexsublem  18032  alexsubALTlem2  18036  alexsubALTlem3  18037  ptcmplem3  18042  ptcmplem4  18043  ptcmplem5  18044  cnextfun  18052  tmdgsum2  18083  symgtgp  18088  tsmsval2  18116  tsmsgsum  18125  utoptop  18221  ismet2  18320  blin  18408  metss2lem  18498  methaus  18507  met1stc  18508  met2ndci  18509  prdsxmslem2  18516  metcnp3  18527  metcnpi3  18533  metusttoOLD  18544  metustto  18545  metustfbasOLD  18552  metustfbas  18553  nlmvscn  18680  nrginvrcn  18684  xrsxmet  18797  reconnlem1  18814  reconn  18816  xrge0tsms  18822  xmetdcn2  18825  metdscn  18843  addcnlem  18851  fsumcn  18857  cnheiborlem  18936  cnheibor  18937  bndth  18940  lebnum  18946  nmoleub2lem2  19081  ipcn  19157  iscmet3  19203  caubl  19217  minveclem3b  19286  minveclem7  19293  pjthlem2  19296  pmltpc  19304  volfiniun  19398  ioombl1  19413  dyadss  19443  dyaddisjlem  19444  dyadmax  19447  dyadmbllem  19448  opnmbllem  19450  itg1addlem2  19546  itg10a  19559  mbfi1fseqlem6  19569  itg2seq  19591  itg2monolem1  19599  itg2gt0  19609  itgfsum  19675  limcfval  19716  ellimc2  19721  ellimc3  19723  limcres  19730  limciun  19738  dvres  19755  dveflem  19820  rolle  19831  dvlip2  19836  c1liplem1  19837  dvgt0lem1  19843  dvgt0  19845  dvlt0  19846  dvne0  19852  dvfsumrlimge0  19871  ftc1lem6  19882  itgsubst  19890  evlslem1  19893  mdegmullem  19958  ply1domn  20003  ply1divex  20016  fta1g  20047  fta1b  20049  plyf  20074  dgrlem  20105  coeid  20114  plydivalg  20173  aannenlem1  20202  aalioulem3  20208  aalioulem6  20211  abelthlem8  20312  efif1olem4  20404  chordthm  20635  xrlimcnp  20764  jensen  20784  sqf11  20879  fsumvma2  20955  perfectlem2  20971  lgsdilem  21063  lgsquad2lem2  21100  lgsquad3  21102  2sqlem5  21109  2sqlem9  21114  2sqb  21119  rpvmasumlem  21138  dchrisum0flb  21161  dchrisum0  21171  pntpbnd  21239  pntibndlem3  21243  pntleml  21262  cusgrarn  21425  usgrasscusgra  21449  4cycl4dv4e  21612  eupath2  21659  vacn  22147  blocni  22263  ubthlem3  22331  minvecolem7  22342  chocunii  22760  pjhthmo  22761  pjhthlem2  22851  kbass5  23580  mdsymlem5  23867  xrofsup  24083  gsumpropd2lem  24177  xrge0tsmsd  24180  qqhval2  24323  volmeas  24544  ballotlemfc0  24707  ballotlemfcc  24708  lgamcvglem  24781  lgamcvg2  24796  derangenlem  24814  erdsze2lem1  24846  pconcon  24875  conpcon  24879  cvxscon  24887  cvmliftmolem2  24926  cvmliftmo  24928  cvmlift2lem10  24956  cvmlift2lem12  24958  cvmlift3lem7  24969  dedekind  25144  prodmolem2  25218  poseq  25471  brcgr  25747  brbtwn2  25752  colinearalg  25757  axsegcon  25774  axeuclidlem  25809  axcontlem9  25819  ifscgr  25886  cgrxfr  25897  btwnconn1lem13  25941  btwnconn1lem14  25942  outsideofeq  25972  ellines  25994  supaddc  26141  mblfinlem  26147  mblfinlem2  26148  itg2addnclem  26159  itg2addnc  26162  ftc1cnnc  26182  finminlem  26215  locfincmp  26278  comppfsc  26281  fnejoin2  26292  upixp  26325  filbcmb  26336  sstotbnd2  26377  isbnd3  26387  prdsbnd2  26398  cntotbnd  26399  ismtyima  26406  bfp  26427  rrncmslem  26435  unichnidl  26535  nacsfix  26660  mzpsubst  26699  mzpcompact2lem  26702  eldioph2lem2  26713  eldioph2  26714  eldioph2b  26715  diophin  26725  diophun  26726  irrapxlem3  26781  irrapxlem5  26783  pell1234qrreccl  26811  pell1234qrmulcl  26812  pell14qrdich  26826  pell1qrge1  26827  pell1qrgaplem  26830  monotuz  26898  rpexpmord  26905  acongtr  26937  acongrep  26939  jm2.23  26961  jm2.26a  26965  jm2.26lem3  26966  jm2.26  26967  jm2.27  26973  wepwsolem  27010  fnwe2lem2  27020  kelac1  27033  kercvrlsm  27053  uvcf1  27113  frlmsslsp  27120  frlmup1  27122  hbtlem5  27204  hbt  27206  mpaaeu  27227  f1otrspeq  27262  psgneu  27301  mamucl  27328  mamulid  27330  mamurid  27331  mamuass  27332  mamudi  27333  mamudir  27334  mamuvs1  27335  mamuvs2  27336  cncmpmax  27574  rfcnnnub  27578  stoweidlem31  27651  stoweidlem34  27654  stoweidlem35  27655  stoweidlem49  27669  stoweidlem59  27679  stoweidlem62  27682  swrdccatin12c  28032  usg2spthonot1  28091  usgfidegfi  28094  usg2spot2nb  28172  lshpcmp  29475  islshpat  29504  lfl0f  29556  ishlat3N  29841  3dim1  29953  islvol5  30065  lvoli2  30067  lncvrelatN  30267  pclfinclN  30436  pexmidlem8N  30463  idltrn  30636  cdleme42keg  30972  cdleme42mgN  30974  cdlemf2  31048  cdlemg2cex  31077  trlcoat  31209  dihopelvalcpre  31735  dih1dimatlem  31816  dihjatcclem4  31908  lcfl7N  31988  lcfrlem9  32037  mapdh9a  32277  hdmapglem7  32419
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-an 361
  Copyright terms: Public domain W3C validator