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

Theorem simplrr 769
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 462 . 2  |-  ( ( ps  /\  ch )  ->  ch )
21ad2antlr 731 1  |-  ( ( ( ph  /\  ( ps  /\  ch ) )  /\  th )  ->  ch )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370
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 188  df-an 372
This theorem is referenced by:  rmob  3329  disjxiun  4358  fsnex  6135  f1prex  6136  isotr  6181  weniso  6199  riota5f  6230  tfrlem9a  7054  oaass  7212  oeeui  7253  oaabs2  7296  resixpfo  7510  omxpenlem  7621  pw2f1olem  7624  fopwdom  7628  fofinf1o  7800  marypha1lem  7895  ordiso2  7978  oismo  8003  ixpiunwdom  8054  cantnf  8145  fseqenlem1  8401  iunfictbso  8491  dfac12lem2  8520  dfac12lem3  8521  infunsdom1  8589  infpssrlem5  8683  fin23lem24  8698  isf32lem2  8730  isf32lem4  8732  isf34lem4  8753  fin1a2lem12  8787  fin1a2lem13  8788  ttukeylem6  8890  fpwwe2lem12  9012  fpwwe2lem13  9013  fpwwe2  9014  winalim2  9067  wunex2  9109  tskord  9151  prlem934  9404  mulcmpblnr  9441  dedekind  9743  addid1  9759  cnegex  9760  negeu  9811  add20  10072  divdivdiv  10254  ltmul12a  10407  lemul12a  10409  lediv12a  10445  supaddc  10520  supmul1  10522  cru  10547  uzwo3  11205  xleadd1a  11485  xmullem  11496  xmulgt0  11515  xlemul1a  11520  ixxun  11597  ixxss12  11601  ioodisj  11708  fz0fzelfz0  11842  mulexpz  12257  leexp1a  12276  expmulnbnd  12349  hashf1  12563  fi1uzind  12593  brfi1indALT  12596  reuccats1  12778  abs3lem  13340  rexanre  13348  cau3lem  13356  limsupgre  13480  limsupgreOLD  13481  limsupbnd2  13484  limsupbnd2OLD  13485  o1lo1  13539  rlimclim1  13547  rlimclim  13548  rlimcn1  13590  rlimcn2  13592  o1of2  13614  o1rlimmul  13620  lo1add  13628  lo1mul  13629  isercolllem1  13666  climcau  13672  caucvgrlem  13674  caucvgrlemOLD  13675  caucvgb  13684  summolem2  13720  summo  13721  modfsummod  13792  o1fsum  13811  prodmolem2  13927  isprm5  14589  isprm6  14604  rpdvds  14614  pclem  14726  pcqmul  14741  pcexp  14747  pcneg  14761  pcprmpw2  14769  pcadd  14772  pcmpt  14775  4sqlem13OLD  14839  4sqlem13  14845  vdwlem2  14870  vdwlem7  14875  vdwlem12  14880  ramval  14898  ramvalOLD  14899  ramub2  14909  ramz2  14920  ramcl  14925  cshwshashlem2  15005  imasval  15349  imasvalOLD  15350  imasdsval  15354  imasdsvalOLD  15366  mreexexd  15492  acsfn  15503  issubc3  15692  idfucl  15724  funcres2c  15744  isnat  15790  fucpropd  15820  xpcval  16000  xpcco  16006  prfval  16022  evlf2  16041  evlfcl  16045  curf12  16050  curf1cl  16051  curf2  16052  curfcl  16055  curf2ndf  16070  hof2val  16079  hofcl  16082  hofpropd  16090  yonedalem4a  16098  yonedainv  16104  drsdirfi  16121  pospo  16157  poslubmo  16330  posglbmo  16331  isipodrs  16345  acsinfd  16364  gsumvalx  16451  gsumpropd2lem  16454  ismndd  16497  mndpropd  16500  mhmeql  16549  mrcmndind  16551  frmdup3lem  16588  mhmmnd  16746  issubg4  16774  ssnmz  16797  conjnmzb  16855  f1otrspeq  17026  psgneu  17085  pgpfi  17195  sylow2blem3  17212  slwhash  17214  fislw  17215  sylow3lem2  17218  lsmdisj2  17270  pj1eu  17284  efgredlem  17335  frgpuplem  17360  gexex  17429  frgpnabl  17449  dprdfadd  17591  dpjidcl  17629  pgpfac1lem3  17648  pgpfaclem3  17654  ablfac2  17660  ringpropd  17750  islmhm2  18199  lmhmpropd  18234  lbsextlem4  18322  assapropd  18489  psrval  18524  evlslem1  18676  prmirredlem  19001  psgndiflemA  19106  lsmcss  19192  uvcf1  19287  frlmsslsp  19291  frlmup1  19293  mamucl  19363  mamuass  19364  mamudi  19365  mamudir  19366  mamuvs1  19367  mamuvs2  19368  mamulid  19403  mamurid  19404  dmatsubcl  19460  dmatmulcl  19462  scmatscm  19475  marrepval  19524  marepveval  19530  mdetunilem7  19580  gsummatr01lem4  19620  cpmatmcllem  19679  mat2pmatf1  19690  mat2pmatlin  19696  decpmatmul  19733  pm2mpmhmlem2  19780  chpidmat  19808  pptbas  19960  toponmre  20046  restbas  20111  iscncl  20222  cnrest2  20239  cnpdis  20246  lmcnp  20257  dishaus  20335  cmpcovf  20343  tgcmp  20353  dfcon2  20371  clscon  20382  2ndcctbss  20407  dis2ndc  20412  1stccnp  20414  islly2  20436  cldllycmp  20447  locfincmp  20478  comppfsc  20484  kgentopon  20490  txcls  20556  ptpjopn  20564  dfac14  20570  xkoccn  20571  txcnp  20572  txcmpb  20596  txlm  20600  xkopt  20607  xkoco1cn  20609  xkoco2cn  20610  qtopcn  20666  qtoprest  20669  regr1lem2  20692  xkocnv  20766  qtophmeo  20769  fmfnfmlem4  20909  hausflim  20933  hauspwpwf1  20939  fclscmp  20982  alexsublem  20996  alexsubALTlem2  21000  alexsubALTlem3  21001  ptcmplem3  21006  ptcmplem4  21007  ptcmplem5  21008  cnextfun  21016  tmdgsum2  21048  symgtgp  21053  tsmsval2  21081  tsmsgsum  21090  utoptop  21186  ismet2  21285  blin  21373  metss2lem  21463  methaus  21472  met1stc  21473  met2ndci  21474  prdsxmslem2  21481  metcnp3  21492  metcnpi3  21498  metustto  21505  metustfbas  21509  nlmvscn  21627  nrginvrcn  21631  xrsxmet  21764  reconnlem1  21781  reconn  21783  xrge0tsms  21789  xmetdcn2  21792  metdscn  21810  metdscnOLD  21825  addcnlem  21833  fsumcn  21839  cnheiborlem  21919  cnheibor  21920  bndth  21923  lebnum  21932  nmoleub2lem2  22067  ipcn  22154  iscmet3  22200  caubl  22214  rrxdstprj1  22300  minveclem3b  22307  minveclem7  22314  minveclem3bOLD  22319  minveclem7OLD  22326  pjthlem2  22329  pmltpc  22338  volfiniun  22437  ioombl1  22452  dyadss  22489  dyaddisjlem  22490  dyadmax  22493  dyadmbllem  22494  opnmbllem  22496  itg1addlem2  22592  itg10a  22605  mbfi1fseqlem6  22615  itg2seq  22637  itg2monolem1  22645  itg2gt0  22655  itgfsum  22721  limcfval  22764  ellimc2  22769  ellimc3  22771  limcres  22778  limciun  22786  dvres  22803  dveflem  22868  rolle  22879  dvlip2  22884  c1liplem1  22885  dvgt0lem1  22891  dvgt0  22893  dvlt0  22894  dvne0  22900  dvfsumrlimge0  22919  ftc1lem6  22930  itgsubst  22938  mdegmullem  22964  ply1domn  23009  ply1divex  23024  fta1g  23055  fta1b  23057  plyf  23089  dgrlem  23120  coeid  23129  plydivalg  23189  aannenlem1  23221  aalioulem3  23227  aalioulem6  23230  abelthlem8  23331  efif1olem4  23431  chordthm  23700  xrlimcnp  23831  jensen  23851  lgamcvglem  23902  lgamcvg2  23917  sqf11  24003  fsumvma2  24079  perfectlem2  24095  lgsdilem  24187  lgsquad2lem2  24224  lgsquad3  24226  2sqlem5  24233  2sqlem9  24238  2sqb  24243  rpvmasumlem  24262  dchrisum0flb  24285  dchrisum0  24295  pntpbnd  24363  pntibndlem3  24367  pntleml  24386  legov  24567  legtrid  24573  tglinethru  24618  tglnpt2  24623  tglineintmo  24624  mirreu3  24636  perpcom  24695  colperpexlem3  24711  mideu  24717  opphllem1  24726  hlpasch  24735  lnopp2hpgb  24742  trgcopy  24783  brcgr  24867  brbtwn2  24872  colinearalg  24877  axsegcon  24894  axeuclidlem  24929  axcontlem9  24939  ecgrtg  24950  elntg  24951  eengtrkg  24952  cusgrarn  25124  usgrasscusgra  25148  4cycl4dv4e  25333  wwlkext2clwwlk  25468  usg2spthonot1  25555  usgfidegfi  25575  eupath2  25645  usg2spot2nb  25730  numclwwlk6  25778  vacn  26267  blocni  26383  ubthlem3  26451  minvecolem7  26462  minvecolem7OLD  26472  chocunii  26891  pjhthmo  26892  pjhthlem2  26982  kbass5  27710  mdsymlem5  27997  foresf1o  28077  fcobij  28255  xrofsup  28298  archirngz  28452  archiabllem2a  28457  xrge0tsmsd  28495  isarchiofld  28527  smatrcl  28569  reff  28613  ordtconlem1  28677  qqhval2  28733  volmeas  29001  fiunelcarsg  29095  ballotlemfc0  29272  ballotlemfcc  29273  signstfvneq0  29408  derangenlem  29841  erdsze2lem1  29873  pconcon  29901  conpcon  29905  cvxscon  29913  cvmliftmolem2  29952  cvmliftmo  29954  cvmlift2lem10  29982  cvmlift2lem12  29984  cvmlift3lem7  29995  mrsubff1  30099  msubff1  30141  poseq  30437  ifscgr  30755  cgrxfr  30766  btwnconn1lem13  30810  btwnconn1lem14  30811  outsideofeq  30841  ellines  30863  finminlem  30918  fnejoin2  30969  poimirlem13  31860  poimirlem14  31861  poimirlem32  31879  opnmbllem0  31883  mblfinlem3  31886  itg2addnclem  31900  itg2addnc  31903  ftc1cnnc  31923  upixp  31963  filbcmb  31974  sstotbnd2  32013  isbnd3  32023  prdsbnd2  32034  cntotbnd  32035  ismtyima  32042  bfp  32063  rrncmslem  32071  unichnidl  32171  lshpcmp  32466  islshpat  32495  lfl0f  32547  ishlat3N  32832  3dim1  32944  islvol5  33056  lvoli2  33058  lncvrelatN  33258  pclfinclN  33427  pexmidlem8N  33454  idltrn  33627  cdleme42keg  33965  cdleme42mgN  33967  cdlemf2  34041  cdlemg2cex  34070  trlcoat  34202  dihopelvalcpre  34728  dih1dimatlem  34809  dihjatcclem4  34901  lcfl7N  34981  lcfrlem9  35030  mapdh9a  35270  hdmapglem7  35412  nacsfix  35466  mzpsubst  35502  mzpcompact2lem  35505  eldioph2lem2  35515  eldioph2  35516  eldioph2b  35517  diophin  35527  diophun  35528  irrapxlem3  35581  irrapxlem5  35583  pell1234qrreccl  35613  pell1234qrmulcl  35614  pell14qrdich  35628  pell1qrge1  35629  pell1qrgaplem  35632  monotuz  35702  rpexpmord  35709  acongtr  35741  acongrep  35743  jm2.23  35764  jm2.26a  35768  jm2.26lem3  35769  jm2.26  35770  jm2.27  35776  wepwsolem  35813  fnwe2lem2  35822  kelac1  35834  kercvrlsm  35854  hbtlem5  35900  hbt  35902  mpaaeu  35929  cncmpmax  37269  rfcnnnub  37273  disjxp1  37327  iccintsng  37516  lptioo2  37594  lptioo1  37595  limclner  37615  stoweidlem31  37775  stoweidlem34  37778  stoweidlem35  37779  stoweidlem49  37793  stoweidlem59  37803  stoweidlem62  37806  stoweidlem62OLD  37807  fourierdlem60  37913  fourierdlem61  37914  fourierdlem87  37940  iundjiun  38149  ismeannd  38156  hoidmvle  38269  perfectALTVlem2  38657  bgoldbtbndlem2  38714  bgoldbtbndlem3  38715  reuccatpfxs1  38788  upgr1opALT  38975  usgredg4  39044  subuhgr  39095  subumgr  39097  usgedgvadf1lem2  39317  usgedgvadf1ALTlem2  39320  mgmhmeql  39394  mndpsuppss  39749  scmsuppss  39750  lindslinindsimp2lem5  39848  elfzolborelfzop1  39909  elbigolo1  39961
  Copyright terms: Public domain W3C validator