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  2647  rmob  3209  disjxiun  4169  isotr  6015  weniso  6034  riota5f  6533  tfrlem9a  6606  oaass  6763  oeeui  6804  oaabs2  6847  resixpfo  7059  omxpenlem  7168  pw2f1olem  7171  fopwdom  7175  fofinf1o  7346  marypha1lem  7396  ordiso2  7440  oismo  7465  ixpiunwdom  7515  cantnf  7605  fseqenlem1  7861  iunfictbso  7951  dfac12lem2  7980  dfac12lem3  7981  infunsdom1  8049  infpssrlem5  8143  fin23lem24  8158  isf32lem2  8190  isf32lem4  8192  isf34lem4  8213  fin1a2lem12  8247  fin1a2lem13  8248  ttukeylem6  8350  fpwwe2lem12  8472  fpwwe2lem13  8473  fpwwe2  8474  winalim2  8527  wunex2  8569  tskord  8611  prlem934  8866  addid1  9202  cnegex  9203  negeu  9252  add20  9496  divdivdiv  9671  ltmul12a  9822  lemul12a  9824  lediv12a  9859  supmul1  9929  cru  9948  uzwo3  10525  xleadd1a  10788  xmullem  10799  xmulgt0  10818  xlemul1a  10823  ixxun  10888  ixxss12  10892  ioodisj  10982  mulexpz  11375  leexp1a  11393  expmulnbnd  11466  hashf1  11661  brfi1uzind  11670  abs3lem  12097  rexanre  12105  cau3lem  12113  limsupgre  12230  limsupbnd2  12232  o1lo1  12286  rlimclim1  12294  rlimclim  12295  rlimcn1  12337  rlimcn2  12339  o1of2  12361  o1rlimmul  12367  lo1add  12375  lo1mul  12376  isercolllem1  12413  climcau  12419  caucvgrlem  12421  caucvgb  12428  summolem2  12465  summo  12466  o1fsum  12547  isprm6  13064  isprm5  13067  rpdvds  13079  pclem  13167  pcqmul  13182  pcexp  13188  pcneg  13202  pcprmpw2  13210  pcadd  13213  pcmpt  13216  4sqlem13  13280  vdwlem2  13305  vdwlem7  13310  vdwlem12  13315  ramval  13331  ramub2  13337  ramz2  13347  ramcl  13352  imasval  13692  imasdsval  13696  mreexexd  13828  acsfn  13839  issubc3  14001  idfucl  14033  funcres2c  14053  isnat  14099  fucpropd  14129  xpcval  14229  xpcco  14235  prfval  14251  evlf2  14270  evlfcl  14274  curf12  14279  curf1cl  14280  curf2  14281  curfcl  14284  curf2ndf  14299  hof2val  14308  hofcl  14311  hofpropd  14319  yonedalem4a  14327  yonedainv  14333  drsdirfi  14350  pospo  14385  poslubmo  14528  isipodrs  14542  acsinfd  14561  mndpropd  14676  mhmeql  14719  gsumvalx  14729  frmdup3  14766  issubg4  14916  ssnmz  14937  conjnmzb  14995  pgpfi  15194  sylow2blem3  15211  slwhash  15213  fislw  15214  sylow3lem2  15217  lsmdisj2  15269  pj1eu  15283  efgredlem  15334  frgpuplem  15359  gexex  15423  frgpnabl  15441  dprdfadd  15533  dpjidcl  15571  pgpfac1lem3  15590  pgpfaclem3  15596  ablfac2  15602  rngpropd  15650  islmhm2  16069  lmhmpropd  16100  lbsextlem4  16188  assapropd  16341  psrval  16384  prmirredlem  16728  lsmcss  16874  pptbas  17027  toponmre  17112  restbas  17176  iscncl  17287  cnrest2  17304  cnpdis  17311  lmcnp  17322  dishaus  17400  cmpcovf  17408  tgcmp  17418  dfcon2  17435  clscon  17446  2ndcctbss  17471  dis2ndc  17476  1stccnp  17478  islly2  17500  cldllycmp  17511  kgentopon  17523  txcls  17589  ptpjopn  17597  dfac14  17603  xkoccn  17604  txcnp  17605  txcmpb  17629  txlm  17633  xkopt  17640  xkoco1cn  17642  xkoco2cn  17643  qtopcn  17699  qtoprest  17702  regr1lem2  17725  xkocnv  17799  qtophmeo  17802  fmfnfmlem4  17942  hausflim  17966  hauspwpwf1  17972  fclscmp  18015  alexsublem  18028  alexsubALTlem2  18032  alexsubALTlem3  18033  ptcmplem3  18038  ptcmplem4  18039  ptcmplem5  18040  cnextfun  18048  tmdgsum2  18079  symgtgp  18084  tsmsval2  18112  tsmsgsum  18121  utoptop  18217  ismet2  18316  blin  18404  metss2lem  18494  methaus  18503  met1stc  18504  met2ndci  18505  prdsxmslem2  18512  metcnp3  18523  metcnpi3  18529  metusttoOLD  18540  metustto  18541  metustfbasOLD  18548  metustfbas  18549  nlmvscn  18676  nrginvrcn  18680  xrsxmet  18793  reconnlem1  18810  reconn  18812  xrge0tsms  18818  xmetdcn2  18821  metdscn  18839  addcnlem  18847  fsumcn  18853  cnheiborlem  18932  cnheibor  18933  bndth  18936  lebnum  18942  nmoleub2lem2  19077  ipcn  19153  iscmet3  19199  caubl  19213  minveclem3b  19282  minveclem7  19289  pjthlem2  19292  pmltpc  19300  volfiniun  19394  ioombl1  19409  dyadss  19439  dyaddisjlem  19440  dyadmax  19443  dyadmbllem  19444  opnmbllem  19446  itg1addlem2  19542  itg10a  19555  mbfi1fseqlem6  19565  itg2seq  19587  itg2monolem1  19595  itg2gt0  19605  itgfsum  19671  limcfval  19712  ellimc2  19717  ellimc3  19719  limcres  19726  limciun  19734  dvres  19751  dveflem  19816  rolle  19827  dvlip2  19832  c1liplem1  19833  dvgt0lem1  19839  dvgt0  19841  dvlt0  19842  dvne0  19848  dvfsumrlimge0  19867  ftc1lem6  19878  itgsubst  19886  evlslem1  19889  mdegmullem  19954  ply1domn  19999  ply1divex  20012  fta1g  20043  fta1b  20045  plyf  20070  dgrlem  20101  coeid  20110  plydivalg  20169  aannenlem1  20198  aalioulem3  20204  aalioulem6  20207  abelthlem8  20308  efif1olem4  20400  chordthm  20631  xrlimcnp  20760  jensen  20780  sqf11  20875  fsumvma2  20951  perfectlem2  20967  lgsdilem  21059  lgsquad2lem2  21096  lgsquad3  21098  2sqlem5  21105  2sqlem9  21110  2sqb  21115  rpvmasumlem  21134  dchrisum0flb  21157  dchrisum0  21167  pntpbnd  21235  pntibndlem3  21239  pntleml  21258  cusgrarn  21421  usgrasscusgra  21445  4cycl4dv4e  21608  eupath2  21655  vacn  22143  blocni  22259  ubthlem3  22327  minvecolem7  22338  chocunii  22756  pjhthmo  22757  pjhthlem2  22847  kbass5  23576  mdsymlem5  23863  xrofsup  24079  gsumpropd2lem  24173  xrge0tsmsd  24176  qqhval2  24319  volmeas  24540  ballotlemfc0  24703  ballotlemfcc  24704  lgamcvglem  24777  lgamcvg2  24792  derangenlem  24810  erdsze2lem1  24842  pconcon  24871  conpcon  24875  cvxscon  24883  cvmliftmolem2  24922  cvmliftmo  24924  cvmlift2lem10  24952  cvmlift2lem12  24954  cvmlift3lem7  24965  dedekind  25140  prodmolem2  25214  poseq  25467  brcgr  25743  brbtwn2  25748  colinearalg  25753  axsegcon  25770  axeuclidlem  25805  axcontlem9  25815  ifscgr  25882  cgrxfr  25893  btwnconn1lem13  25937  btwnconn1lem14  25938  outsideofeq  25968  ellines  25990  supaddc  26137  mblfinlem  26143  mblfinlem2  26144  itg2addnclem  26155  itg2addnc  26158  ftc1cnnc  26178  finminlem  26211  locfincmp  26274  comppfsc  26277  fnejoin2  26288  upixp  26321  filbcmb  26332  sstotbnd2  26373  isbnd3  26383  prdsbnd2  26394  cntotbnd  26395  ismtyima  26402  bfp  26423  rrncmslem  26431  unichnidl  26531  nacsfix  26656  mzpsubst  26695  mzpcompact2lem  26698  eldioph2lem2  26709  eldioph2  26710  eldioph2b  26711  diophin  26721  diophun  26722  irrapxlem3  26777  irrapxlem5  26779  pell1234qrreccl  26807  pell1234qrmulcl  26808  pell14qrdich  26822  pell1qrge1  26823  pell1qrgaplem  26826  monotuz  26894  rpexpmord  26901  acongtr  26933  acongrep  26935  jm2.23  26957  jm2.26a  26961  jm2.26lem3  26962  jm2.26  26963  jm2.27  26969  wepwsolem  27006  fnwe2lem2  27016  kelac1  27029  kercvrlsm  27049  uvcf1  27109  frlmsslsp  27116  frlmup1  27118  hbtlem5  27200  hbt  27202  mpaaeu  27223  f1otrspeq  27258  psgneu  27297  mamucl  27324  mamulid  27326  mamurid  27327  mamuass  27328  mamudi  27329  mamudir  27330  mamuvs1  27331  mamuvs2  27332  cncmpmax  27570  rfcnnnub  27574  stoweidlem31  27647  stoweidlem34  27650  stoweidlem35  27651  stoweidlem49  27665  stoweidlem59  27675  stoweidlem62  27678  swrdccatin12c  28028  usg2spthonot1  28087  usgfidegfi  28090  usg2spot2nb  28168  lshpcmp  29471  islshpat  29500  lfl0f  29552  ishlat3N  29837  3dim1  29949  islvol5  30061  lvoli2  30063  lncvrelatN  30263  pclfinclN  30432  pexmidlem8N  30459  idltrn  30632  cdleme42keg  30968  cdleme42mgN  30970  cdlemf2  31044  cdlemg2cex  31073  trlcoat  31205  dihopelvalcpre  31731  dih1dimatlem  31812  dihjatcclem4  31904  lcfl7N  31984  lcfrlem9  32033  mapdh9a  32273  hdmapglem7  32415
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