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

Theorem simplrr 737
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 447 . 2  |-  ( ( ps  /\  ch )  ->  ch )
21ad2antlr 707 1  |-  ( ( ( ph  /\  ( ps  /\  ch ) )  /\  th )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358
This theorem is referenced by:  pm2.61da3ne  2559  rmob  3113  disjxiun  4057  isotr  5875  weniso  5894  riota5f  6371  tfrlem9a  6444  oaass  6601  oeeui  6642  oaabs2  6685  resixpfo  6897  omxpenlem  7006  pw2f1olem  7009  fopwdom  7013  fofinf1o  7182  marypha1lem  7231  ordiso2  7275  oismo  7300  ixpiunwdom  7350  cantnf  7440  fseqenlem1  7696  iunfictbso  7786  dfac12lem2  7815  dfac12lem3  7816  infunsdom1  7884  infpssrlem5  7978  fin23lem24  7993  isf32lem2  8025  isf32lem4  8027  isf34lem4  8048  fin1a2lem12  8082  fin1a2lem13  8083  ttukeylem6  8186  fpwwe2lem12  8308  fpwwe2lem13  8309  fpwwe2  8310  winalim2  8363  wunex2  8405  tskord  8447  prlem934  8702  addid1  9037  cnegex  9038  negeu  9087  add20  9331  divdivdiv  9506  ltmul12a  9657  lemul12a  9659  lediv12a  9694  supmul1  9764  cru  9783  uzwo3  10358  xleadd1a  10620  xmullem  10631  xmulgt0  10650  xlemul1a  10655  ixxun  10719  ixxss12  10723  ioodisj  10812  mulexpz  11189  leexp1a  11207  expmulnbnd  11280  hashf1  11442  abs3lem  11869  rexanre  11877  cau3lem  11885  limsupgre  12002  limsupbnd2  12004  o1lo1  12058  rlimclim1  12066  rlimclim  12067  rlimcn1  12109  rlimcn2  12111  o1of2  12133  o1rlimmul  12139  lo1add  12147  lo1mul  12148  isercolllem1  12185  climcau  12191  caucvgrlem  12192  caucvgb  12199  summolem2  12236  summo  12237  o1fsum  12318  isprm6  12835  isprm5  12838  rpdvds  12850  pclem  12938  pcqmul  12953  pcexp  12959  pcneg  12973  pcprmpw2  12981  pcadd  12984  pcmpt  12987  4sqlem13  13051  vdwlem2  13076  vdwlem7  13081  vdwlem12  13086  ramval  13102  ramub2  13108  ramz2  13118  ramcl  13123  imasval  13463  imasdsval  13467  mreexexd  13599  acsfn  13610  issubc3  13772  idfucl  13804  funcres2c  13824  isnat  13870  fucpropd  13900  xpcval  14000  xpcco  14006  prfval  14022  evlf2  14041  evlfcl  14045  curf12  14050  curf1cl  14051  curf2  14052  curfcl  14055  curf2ndf  14070  hof2val  14079  hofcl  14082  hofpropd  14090  yonedalem4a  14098  yonedainv  14104  drsdirfi  14121  pospo  14156  poslubmo  14299  isipodrs  14313  acsinfd  14332  mndpropd  14447  mhmeql  14490  gsumvalx  14500  frmdup3  14537  issubg4  14687  ssnmz  14708  conjnmzb  14766  pgpfi  14965  sylow2blem3  14982  slwhash  14984  fislw  14985  sylow3lem2  14988  lsmdisj2  15040  pj1eu  15054  efgredlem  15105  frgpuplem  15130  gexex  15194  frgpnabl  15212  dprdfadd  15304  dpjidcl  15342  pgpfac1lem3  15361  pgpfaclem3  15367  ablfac2  15373  rngpropd  15421  islmhm2  15844  lmhmpropd  15875  lbsextlem4  15963  assapropd  16116  psrval  16159  prmirredlem  16502  lsmcss  16648  pptbas  16801  toponmre  16886  restbas  16945  iscncl  17054  cnrest2  17070  cnpdis  17077  lmcnp  17088  dishaus  17166  cmpcovf  17174  tgcmp  17184  dfcon2  17201  clscon  17212  2ndcctbss  17237  dis2ndc  17242  1stccnp  17244  islly2  17266  cldllycmp  17277  kgentopon  17289  txcls  17355  ptpjopn  17362  dfac14  17368  xkoccn  17369  txcnp  17370  txcmpb  17394  txlm  17398  xkopt  17405  xkoco1cn  17407  xkoco2cn  17408  qtopcn  17461  qtoprest  17464  regr1lem2  17487  xkocnv  17561  qtophmeo  17564  fmfnfmlem4  17704  hausflim  17728  hauspwpwf1  17734  fclscmp  17777  alexsublem  17790  alexsubALTlem2  17794  alexsubALTlem3  17795  ptcmplem3  17800  ptcmplem4  17801  ptcmplem5  17802  tmdgsum2  17831  symgtgp  17836  tsmsval2  17864  tsmsgsum  17873  ismet2  17950  blin  18022  metss2lem  18109  methaus  18118  met1stc  18119  met2ndci  18120  prdsxmslem2  18127  metcnp3  18138  metcnpi3  18144  nlmvscn  18250  nrginvrcn  18254  xrsxmet  18367  reconnlem1  18383  reconn  18385  xrge0tsms  18391  xmetdcn2  18394  metdscn  18412  addcnlem  18420  fsumcn  18426  cnheiborlem  18505  cnheibor  18506  bndth  18509  lebnum  18515  nmoleub2lem2  18650  ipcn  18726  iscmet3  18772  caubl  18786  minveclem3b  18845  minveclem7  18852  pjthlem2  18855  pmltpc  18863  volfiniun  18957  ioombl1  18972  dyadss  19002  dyaddisjlem  19003  dyadmax  19006  dyadmbllem  19007  opnmbllem  19009  itg1addlem2  19105  itg10a  19118  mbfi1fseqlem6  19128  itg2seq  19150  itg2monolem1  19158  itg2gt0  19168  itgfsum  19234  limcfval  19275  ellimc2  19280  ellimc3  19282  limcres  19289  limciun  19297  dvres  19314  dveflem  19379  rolle  19390  dvlip2  19395  c1liplem1  19396  dvgt0lem1  19402  dvgt0  19404  dvlt0  19405  dvne0  19411  dvfsumrlimge0  19430  ftc1lem6  19441  itgsubst  19449  evlslem1  19452  mdegmullem  19517  ply1domn  19562  ply1divex  19575  fta1g  19606  fta1b  19608  plyf  19633  dgrlem  19664  coeid  19673  plydivalg  19732  aannenlem1  19761  aalioulem3  19767  aalioulem6  19770  abelthlem8  19868  efif1olem4  19960  chordthm  20187  xrlimcnp  20316  jensen  20336  sqf11  20430  fsumvma2  20506  perfectlem2  20522  lgsdilem  20614  lgsquad2lem2  20651  lgsquad3  20653  2sqlem5  20660  2sqlem9  20665  2sqb  20670  rpvmasumlem  20689  dchrisum0flb  20712  dchrisum0  20722  pntpbnd  20790  pntibndlem3  20794  pntleml  20813  vacn  21322  blocni  21438  ubthlem3  21506  minvecolem7  21517  chocunii  21935  pjhthmo  21936  pjhthlem2  22026  kbass5  22755  mdsymlem5  23042  xrofsup  23272  gsumpropd2lem  23357  xrge0tsmsd  23360  cnextfun  23414  utoptop  23446  metustto  23495  metustfbas  23499  qqhval2  23561  volmeas  23761  ballotlemfc0  23924  ballotlemfcc  23925  derangenlem  23986  erdsze2lem1  24018  pconcon  24046  conpcon  24050  cvxscon  24058  cvmliftmolem2  24097  cvmliftmo  24099  cvmlift2lem10  24127  cvmlift2lem12  24129  cvmlift3lem7  24140  eupath2  24188  dedekind  24368  prodmolem2  24438  poseq  24638  brcgr  24914  brbtwn2  24919  colinearalg  24924  axsegcon  24941  axeuclidlem  24976  axcontlem9  24986  ifscgr  25053  cgrxfr  25064  btwnconn1lem13  25108  btwnconn1lem14  25109  outsideofeq  25139  ellines  25161  supaddc  25309  itg2addnclem  25317  itg2addnc  25319  ftc1cnnc  25339  finminlem  25380  locfincmp  25453  comppfsc  25456  fnejoin2  25467  upixp  25552  filbcmb  25581  sstotbnd2  25646  isbnd3  25656  prdsbnd2  25667  cntotbnd  25668  ismtyima  25675  bfp  25696  rrncmslem  25704  unichnidl  25804  nacsfix  25935  mzpsubst  25974  mzpcompact2lem  25977  eldioph2lem2  25988  eldioph2  25989  eldioph2b  25990  diophin  26000  diophun  26001  irrapxlem3  26057  irrapxlem5  26059  pell1234qrreccl  26087  pell1234qrmulcl  26088  pell14qrdich  26102  pell1qrge1  26103  pell1qrgaplem  26106  monotuz  26174  rpexpmord  26181  acongtr  26213  acongrep  26215  jm2.23  26237  jm2.26a  26241  jm2.26lem3  26242  jm2.26  26243  jm2.27  26249  wepwsolem  26286  fnwe2lem2  26296  kelac1  26309  kercvrlsm  26329  uvcf1  26389  frlmsslsp  26396  frlmup1  26398  hbtlem5  26480  hbt  26482  mpaaeu  26503  f1otrspeq  26538  psgneu  26577  mamucl  26604  mamulid  26606  mamurid  26607  mamuass  26608  mamudi  26609  mamudir  26610  mamuvs1  26611  mamuvs2  26612  cncmpmax  26851  rfcnnnub  26855  stoweidlem27  26924  stoweidlem31  26928  stoweidlem34  26931  stoweidlem35  26932  stoweidlem49  26946  stoweidlem59  26956  stoweidlem62  26959  4cycl4dv4e  27552  lshpcmp  28996  islshpat  29025  lfl0f  29077  ishlat3N  29362  3dim1  29474  islvol5  29586  lvoli2  29588  lncvrelatN  29788  pclfinclN  29957  pexmidlem8N  29984  idltrn  30157  cdleme42keg  30493  cdleme42mgN  30495  cdlemf2  30569  cdlemg2cex  30598  trlcoat  30730  dihopelvalcpre  31256  dih1dimatlem  31337  dihjatcclem4  31429  lcfl7N  31509  lcfrlem9  31558  mapdh9a  31798  hdmapglem7  31940
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 177  df-an 360
  Copyright terms: Public domain W3C validator