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

Theorem simplrr 760
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 459 . 2  |-  ( ( ps  /\  ch )  ->  ch )
21ad2antlr 724 1  |-  ( ( ( ph  /\  ( ps  /\  ch ) )  /\  th )  ->  ch )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367
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 369
This theorem is referenced by:  pm2.61da3neOLD  2703  rmob  3344  disjxiun  4364  isotr  6133  weniso  6151  riota5f  6182  tfrlem9a  6973  oaass  7128  oeeui  7169  oaabs2  7212  resixpfo  7426  omxpenlem  7537  pw2f1olem  7540  fopwdom  7544  fofinf1o  7716  marypha1lem  7808  ordiso2  7855  oismo  7880  ixpiunwdom  7932  cantnf  8025  cantnfOLD  8047  fseqenlem1  8318  iunfictbso  8408  dfac12lem2  8437  dfac12lem3  8438  infunsdom1  8506  infpssrlem5  8600  fin23lem24  8615  isf32lem2  8647  isf32lem4  8649  isf34lem4  8670  fin1a2lem12  8704  fin1a2lem13  8705  ttukeylem6  8807  fpwwe2lem12  8930  fpwwe2lem13  8931  fpwwe2  8932  winalim2  8985  wunex2  9027  tskord  9069  prlem934  9322  mulcmpblnr  9359  dedekind  9655  addid1  9671  cnegex  9672  negeu  9723  add20  9982  divdivdiv  10162  ltmul12a  10315  lemul12a  10317  lediv12a  10354  supmul1  10424  cru  10444  uzwo3  11096  xleadd1a  11366  xmullem  11377  xmulgt0  11396  xlemul1a  11401  ixxun  11466  ixxss12  11470  ioodisj  11571  fz0fzelfz0  11702  mulexpz  12109  leexp1a  12127  expmulnbnd  12200  hashf1  12410  brfi1uzind  12436  reuccats1  12617  abs3lem  13173  rexanre  13181  cau3lem  13189  limsupgre  13306  limsupbnd2  13308  o1lo1  13362  rlimclim1  13370  rlimclim  13371  rlimcn1  13413  rlimcn2  13415  o1of2  13437  o1rlimmul  13443  lo1add  13451  lo1mul  13452  isercolllem1  13489  climcau  13495  caucvgrlem  13497  caucvgb  13504  summolem2  13540  summo  13541  modfsummod  13610  o1fsum  13629  prodmolem2  13744  isprm6  14252  isprm5  14255  rpdvds  14267  pclem  14364  pcqmul  14379  pcexp  14385  pcneg  14399  pcprmpw2  14407  pcadd  14410  pcmpt  14413  4sqlem13  14477  vdwlem2  14502  vdwlem7  14507  vdwlem12  14512  ramval  14528  ramub2  14534  ramz2  14544  ramcl  14549  cshwshashlem2  14583  imasval  14918  imasdsval  14922  mreexexd  15055  acsfn  15066  issubc3  15255  idfucl  15287  funcres2c  15307  isnat  15353  fucpropd  15383  xpcval  15563  xpcco  15569  prfval  15585  evlf2  15604  evlfcl  15608  curf12  15613  curf1cl  15614  curf2  15615  curfcl  15618  curf2ndf  15633  hof2val  15642  hofcl  15645  hofpropd  15653  yonedalem4a  15661  yonedainv  15667  drsdirfi  15684  pospo  15720  poslubmo  15893  posglbmo  15894  isipodrs  15908  acsinfd  15927  gsumvalx  16014  gsumpropd2lem  16017  ismndd  16060  mndpropd  16063  mhmeql  16112  mrcmndind  16114  frmdup3lem  16151  mhmmnd  16309  issubg4  16337  ssnmz  16360  conjnmzb  16418  f1otrspeq  16589  psgneu  16648  pgpfi  16742  sylow2blem3  16759  slwhash  16761  fislw  16762  sylow3lem2  16765  lsmdisj2  16817  pj1eu  16831  efgredlem  16882  frgpuplem  16907  gexex  16976  frgpnabl  16996  dprdfadd  17173  dprdfaddOLD  17180  dpjidcl  17220  dpjidclOLD  17227  pgpfac1lem3  17241  pgpfaclem3  17247  ablfac2  17253  ringpropd  17343  islmhm2  17797  lmhmpropd  17832  lbsextlem4  17920  assapropd  18089  psrval  18124  evlslem1  18297  prmirredlem  18623  psgndiflemA  18728  lsmcss  18814  uvcf1  18912  frlmsslsp  18916  frlmup1  18918  mamucl  18988  mamuass  18989  mamudi  18990  mamudir  18991  mamuvs1  18992  mamuvs2  18993  mamulid  19028  mamurid  19029  dmatsubcl  19085  dmatmulcl  19087  scmatscm  19100  marrepval  19149  marepveval  19155  mdetunilem7  19205  gsummatr01lem4  19245  cpmatmcllem  19304  mat2pmatf1  19315  mat2pmatlin  19321  decpmatmul  19358  pm2mpmhmlem2  19405  chpidmat  19433  pptbas  19594  toponmre  19680  restbas  19745  iscncl  19856  cnrest2  19873  cnpdis  19880  lmcnp  19891  dishaus  19969  cmpcovf  19977  tgcmp  19987  dfcon2  20005  clscon  20016  2ndcctbss  20041  dis2ndc  20046  1stccnp  20048  islly2  20070  cldllycmp  20081  locfincmp  20112  comppfsc  20118  kgentopon  20124  txcls  20190  ptpjopn  20198  dfac14  20204  xkoccn  20205  txcnp  20206  txcmpb  20230  txlm  20234  xkopt  20241  xkoco1cn  20243  xkoco2cn  20244  qtopcn  20300  qtoprest  20303  regr1lem2  20326  xkocnv  20400  qtophmeo  20403  fmfnfmlem4  20543  hausflim  20567  hauspwpwf1  20573  fclscmp  20616  alexsublem  20629  alexsubALTlem2  20633  alexsubALTlem3  20634  ptcmplem3  20639  ptcmplem4  20640  ptcmplem5  20641  cnextfun  20649  tmdgsum2  20680  symgtgp  20685  tsmsval2  20713  tsmsgsum  20722  tsmsgsumOLD  20725  utoptop  20822  ismet2  20921  blin  21009  metss2lem  21099  methaus  21108  met1stc  21109  met2ndci  21110  prdsxmslem2  21117  metcnp3  21128  metcnpi3  21134  metusttoOLD  21145  metustto  21146  metustfbasOLD  21153  metustfbas  21154  nlmvscn  21281  nrginvrcn  21285  xrsxmet  21399  reconnlem1  21416  reconn  21418  xrge0tsms  21424  xmetdcn2  21427  metdscn  21445  addcnlem  21453  fsumcn  21459  cnheiborlem  21539  cnheibor  21540  bndth  21543  lebnum  21549  nmoleub2lem2  21684  ipcn  21771  iscmet3  21817  caubl  21831  rrxdstprj1  21921  minveclem3b  21928  minveclem7  21935  pjthlem2  21938  pmltpc  21947  volfiniun  22042  ioombl1  22057  dyadss  22088  dyaddisjlem  22089  dyadmax  22092  dyadmbllem  22093  opnmbllem  22095  itg1addlem2  22189  itg10a  22202  mbfi1fseqlem6  22212  itg2seq  22234  itg2monolem1  22242  itg2gt0  22252  itgfsum  22318  limcfval  22361  ellimc2  22366  ellimc3  22368  limcres  22375  limciun  22383  dvres  22400  dveflem  22465  rolle  22476  dvlip2  22481  c1liplem1  22482  dvgt0lem1  22488  dvgt0  22490  dvlt0  22491  dvne0  22497  dvfsumrlimge0  22516  ftc1lem6  22527  itgsubst  22535  mdegmullem  22563  ply1domn  22609  ply1divex  22622  fta1g  22653  fta1b  22655  plyf  22680  dgrlem  22711  coeid  22720  plydivalg  22780  aannenlem1  22809  aalioulem3  22815  aalioulem6  22818  abelthlem8  22919  efif1olem4  23017  chordthm  23284  xrlimcnp  23415  jensen  23435  sqf11  23530  fsumvma2  23606  perfectlem2  23622  lgsdilem  23714  lgsquad2lem2  23751  lgsquad3  23753  2sqlem5  23760  2sqlem9  23765  2sqb  23770  rpvmasumlem  23789  dchrisum0flb  23812  dchrisum0  23822  pntpbnd  23890  pntibndlem3  23894  pntleml  23913  legov  24092  legtrid  24098  tglinethru  24136  tglnpt2  24141  tglineintmo  24142  mirreu3  24155  perpcom  24210  colperpexlem3  24226  mideu  24232  opphllem1  24239  lnopp2hpgb  24252  brcgr  24324  brbtwn2  24329  colinearalg  24334  axsegcon  24351  axeuclidlem  24386  axcontlem9  24396  ecgrtg  24407  elntg  24408  eengtrkg  24409  cusgrarn  24580  usgrasscusgra  24604  4cycl4dv4e  24789  wwlkext2clwwlk  24924  usg2spthonot1  25011  usgfidegfi  25031  eupath2  25101  usg2spot2nb  25186  numclwwlk6  25234  vacn  25721  blocni  25837  ubthlem3  25905  minvecolem7  25916  chocunii  26336  pjhthmo  26337  pjhthlem2  26427  kbass5  27155  mdsymlem5  27442  foresf1o  27521  fcobij  27698  xrofsup  27735  archirngz  27886  archiabllem2a  27891  xrge0tsmsd  27929  isarchiofld  27961  reff  27996  ordtconlem1  28060  qqhval2  28116  volmeas  28359  fiunelcarsg  28443  ballotlemfc0  28614  ballotlemfcc  28615  signstfvneq0  28712  lgamcvglem  28771  lgamcvg2  28786  derangenlem  28804  erdsze2lem1  28836  pconcon  28865  conpcon  28869  cvxscon  28877  cvmliftmolem2  28916  cvmliftmo  28918  cvmlift2lem10  28946  cvmlift2lem12  28948  cvmlift3lem7  28959  mrsubff1  29063  msubff1  29105  poseq  29498  ifscgr  29847  cgrxfr  29858  btwnconn1lem13  29902  btwnconn1lem14  29903  outsideofeq  29933  ellines  29955  supaddc  30206  opnmbllem0  30215  mblfinlem3  30218  itg2addnclem  30232  itg2addnc  30235  ftc1cnnc  30255  finminlem  30302  fnejoin2  30353  upixp  30386  filbcmb  30397  sstotbnd2  30436  isbnd3  30446  prdsbnd2  30457  cntotbnd  30458  ismtyima  30465  bfp  30486  rrncmslem  30494  unichnidl  30594  nacsfix  30810  mzpsubst  30846  mzpcompact2lem  30849  eldioph2lem2  30859  eldioph2  30860  eldioph2b  30861  diophin  30871  diophun  30872  irrapxlem3  30925  irrapxlem5  30927  pell1234qrreccl  30955  pell1234qrmulcl  30956  pell14qrdich  30970  pell1qrge1  30971  pell1qrgaplem  30974  monotuz  31042  rpexpmord  31049  acongtr  31081  acongrep  31083  jm2.23  31104  jm2.26a  31108  jm2.26lem3  31109  jm2.26  31110  jm2.27  31116  wepwsolem  31153  fnwe2lem2  31163  kelac1  31175  kercvrlsm  31195  hbtlem5  31245  hbt  31247  mpaaeu  31267  cncmpmax  31574  rfcnnnub  31578  iccintsng  31729  lptioo2  31803  lptioo1  31804  limclner  31823  stoweidlem31  31979  stoweidlem34  31982  stoweidlem35  31983  stoweidlem49  31997  stoweidlem59  32007  stoweidlem62  32010  fourierdlem60  32115  fourierdlem61  32116  fourierdlem87  32142  perfectALTVlem2  32544  reuccatpfxs1  32609  usgedgvadf1lem2  32732  usgedgvadf1ALTlem2  32735  mgmhmeql  32809  mndpsuppss  33164  scmsuppss  33165  lindslinindsimp2lem5  33263  elfzolborelfzop1  33325  elbigolo1  33378  lshpcmp  35126  islshpat  35155  lfl0f  35207  ishlat3N  35492  3dim1  35604  islvol5  35716  lvoli2  35718  lncvrelatN  35918  pclfinclN  36087  pexmidlem8N  36114  idltrn  36287  cdleme42keg  36625  cdleme42mgN  36627  cdlemf2  36701  cdlemg2cex  36730  trlcoat  36862  dihopelvalcpre  37388  dih1dimatlem  37469  dihjatcclem4  37561  lcfl7N  37641  lcfrlem9  37690  mapdh9a  37930  hdmapglem7  38072
  Copyright terms: Public domain W3C validator