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 461 . 2  |-  ( ( ps  /\  ch )  ->  ch )
21ad2antlr 726 1  |-  ( ( ( ph  /\  ( ps  /\  ch ) )  /\  th )  ->  ch )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369
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 371
This theorem is referenced by:  pm2.61da3ne  2686  rmob  3281  disjxiun  4284  isotr  6022  weniso  6040  riota5f  6072  tfrlem9a  6837  oaass  6992  oeeui  7033  oaabs2  7076  resixpfo  7293  omxpenlem  7404  pw2f1olem  7407  fopwdom  7411  fofinf1o  7584  marypha1lem  7675  ordiso2  7721  oismo  7746  ixpiunwdom  7798  cantnf  7893  cantnfOLD  7915  fseqenlem1  8186  iunfictbso  8276  dfac12lem2  8305  dfac12lem3  8306  infunsdom1  8374  infpssrlem5  8468  fin23lem24  8483  isf32lem2  8515  isf32lem4  8517  isf34lem4  8538  fin1a2lem12  8572  fin1a2lem13  8573  ttukeylem6  8675  fpwwe2lem12  8800  fpwwe2lem13  8801  fpwwe2  8802  winalim2  8855  wunex2  8897  tskord  8939  prlem934  9194  dedekind  9525  addid1  9541  cnegex  9542  negeu  9592  add20  9843  divdivdiv  10024  ltmul12a  10177  lemul12a  10179  lediv12a  10217  supmul1  10287  cru  10306  uzwo3  10940  xleadd1a  11208  xmullem  11219  xmulgt0  11238  xlemul1a  11243  ixxun  11308  ixxss12  11312  ioodisj  11407  fz0fzelfz0  11478  mulexpz  11896  leexp1a  11914  expmulnbnd  11988  hashf1  12202  brfi1uzind  12211  abs3lem  12818  rexanre  12826  cau3lem  12834  limsupgre  12951  limsupbnd2  12953  o1lo1  13007  rlimclim1  13015  rlimclim  13016  rlimcn1  13058  rlimcn2  13060  o1of2  13082  o1rlimmul  13088  lo1add  13096  lo1mul  13097  isercolllem1  13134  climcau  13140  caucvgrlem  13142  caucvgb  13149  summolem2  13185  summo  13186  o1fsum  13268  isprm6  13787  isprm5  13790  rpdvds  13802  pclem  13897  pcqmul  13912  pcexp  13918  pcneg  13932  pcprmpw2  13940  pcadd  13943  pcmpt  13946  4sqlem13  14010  vdwlem2  14035  vdwlem7  14040  vdwlem12  14045  ramval  14061  ramub2  14067  ramz2  14077  ramcl  14082  cshwshashlem2  14115  imasval  14441  imasdsval  14445  mreexexd  14578  acsfn  14589  issubc3  14751  idfucl  14783  funcres2c  14803  isnat  14849  fucpropd  14879  xpcval  14979  xpcco  14985  prfval  15001  evlf2  15020  evlfcl  15024  curf12  15029  curf1cl  15030  curf2  15031  curfcl  15034  curf2ndf  15049  hof2val  15058  hofcl  15061  hofpropd  15069  yonedalem4a  15077  yonedainv  15083  drsdirfi  15100  pospo  15135  poslubmo  15308  posglbmo  15309  isipodrs  15323  acsinfd  15342  mndpropd  15438  mhmeql  15483  mrcmndind  15485  gsumvalx  15493  gsumpropd2lem  15496  frmdup3  15535  issubg4  15691  ssnmz  15714  conjnmzb  15772  f1otrspeq  15944  psgneu  16003  pgpfi  16095  sylow2blem3  16112  slwhash  16114  fislw  16115  sylow3lem2  16118  lsmdisj2  16170  pj1eu  16184  efgredlem  16235  frgpuplem  16260  gexex  16326  frgpnabl  16344  dprdfadd  16498  dprdfaddOLD  16505  dpjidcl  16545  dpjidclOLD  16552  pgpfac1lem3  16566  pgpfaclem3  16572  ablfac2  16578  rngpropd  16664  islmhm2  17096  lmhmpropd  17131  lbsextlem4  17219  assapropd  17375  psrval  17406  evlslem1  17576  prmirredlem  17892  prmirredlemOLD  17895  psgndiflemA  18006  lsmcss  18092  uvcf1  18192  frlmsslsp  18198  frlmsslspOLD  18199  frlmup1  18201  mamucl  18276  mamulid  18279  mamurid  18280  mamuass  18281  mamudi  18282  mamudir  18283  mamuvs1  18284  mamuvs2  18285  marrepval  18348  marepveval  18354  mdetunilem7  18399  gsummatr01lem4  18439  pptbas  18587  toponmre  18672  restbas  18737  iscncl  18848  cnrest2  18865  cnpdis  18872  lmcnp  18883  dishaus  18961  cmpcovf  18969  tgcmp  18979  dfcon2  18998  clscon  19009  2ndcctbss  19034  dis2ndc  19039  1stccnp  19041  islly2  19063  cldllycmp  19074  kgentopon  19086  txcls  19152  ptpjopn  19160  dfac14  19166  xkoccn  19167  txcnp  19168  txcmpb  19192  txlm  19196  xkopt  19203  xkoco1cn  19205  xkoco2cn  19206  qtopcn  19262  qtoprest  19265  regr1lem2  19288  xkocnv  19362  qtophmeo  19365  fmfnfmlem4  19505  hausflim  19529  hauspwpwf1  19535  fclscmp  19578  alexsublem  19591  alexsubALTlem2  19595  alexsubALTlem3  19596  ptcmplem3  19601  ptcmplem4  19602  ptcmplem5  19603  cnextfun  19611  tmdgsum2  19642  symgtgp  19647  tsmsval2  19675  tsmsgsum  19684  tsmsgsumOLD  19687  utoptop  19784  ismet2  19883  blin  19971  metss2lem  20061  methaus  20070  met1stc  20071  met2ndci  20072  prdsxmslem2  20079  metcnp3  20090  metcnpi3  20096  metusttoOLD  20107  metustto  20108  metustfbasOLD  20115  metustfbas  20116  nlmvscn  20243  nrginvrcn  20247  xrsxmet  20361  reconnlem1  20378  reconn  20380  xrge0tsms  20386  xmetdcn2  20389  metdscn  20407  addcnlem  20415  fsumcn  20421  cnheiborlem  20501  cnheibor  20502  bndth  20505  lebnum  20511  nmoleub2lem2  20646  ipcn  20733  iscmet3  20779  caubl  20793  rrxdstprj1  20883  minveclem3b  20890  minveclem7  20897  pjthlem2  20900  pmltpc  20909  volfiniun  21003  ioombl1  21018  dyadss  21049  dyaddisjlem  21050  dyadmax  21053  dyadmbllem  21054  opnmbllem  21056  itg1addlem2  21150  itg10a  21163  mbfi1fseqlem6  21173  itg2seq  21195  itg2monolem1  21203  itg2gt0  21213  itgfsum  21279  limcfval  21322  ellimc2  21327  ellimc3  21329  limcres  21336  limciun  21344  dvres  21361  dveflem  21426  rolle  21437  dvlip2  21442  c1liplem1  21443  dvgt0lem1  21449  dvgt0  21451  dvlt0  21452  dvne0  21458  dvfsumrlimge0  21477  ftc1lem6  21488  itgsubst  21496  mdegmullem  21524  ply1domn  21570  ply1divex  21583  fta1g  21614  fta1b  21616  plyf  21641  dgrlem  21672  coeid  21681  plydivalg  21740  aannenlem1  21769  aalioulem3  21775  aalioulem6  21778  abelthlem8  21879  efif1olem4  21976  chordthm  22207  xrlimcnp  22337  jensen  22357  sqf11  22452  fsumvma2  22528  perfectlem2  22544  lgsdilem  22636  lgsquad2lem2  22673  lgsquad3  22675  2sqlem5  22682  2sqlem9  22687  2sqb  22692  rpvmasumlem  22711  dchrisum0flb  22734  dchrisum0  22744  pntpbnd  22812  pntibndlem3  22816  pntleml  22835  legov  22987  legtrid  22993  tglinethru  23012  tglineintmo  23016  mirreu3  23026  brcgr  23097  brbtwn2  23102  colinearalg  23107  axsegcon  23124  axeuclidlem  23159  axcontlem9  23169  ecgrtg  23180  elntg  23181  eengtrkg  23182  cusgrarn  23318  usgrasscusgra  23342  4cycl4dv4e  23505  eupath2  23552  vacn  24040  blocni  24156  ubthlem3  24224  minvecolem7  24235  chocunii  24655  pjhthmo  24656  pjhthlem2  24746  kbass5  25475  mdsymlem5  25762  fcobij  25976  xrofsup  26006  archirngz  26157  archiabllem2a  26162  xrge0tsmsd  26204  isarchiofld  26236  qqhval2  26363  volmeas  26599  ballotlemfc0  26827  ballotlemfcc  26828  signstfvneq0  26925  lgamcvglem  26978  lgamcvg2  26993  derangenlem  27011  erdsze2lem1  27043  pconcon  27072  conpcon  27076  cvxscon  27084  cvmliftmolem2  27123  cvmliftmo  27125  cvmlift2lem10  27153  cvmlift2lem12  27155  cvmlift3lem7  27166  prodmolem2  27399  poseq  27665  ifscgr  28026  cgrxfr  28037  btwnconn1lem13  28081  btwnconn1lem14  28082  outsideofeq  28112  ellines  28134  supaddc  28370  opnmbllem0  28380  mblfinlem3  28383  itg2addnclem  28396  itg2addnc  28399  ftc1cnnc  28419  finminlem  28466  locfincmp  28529  comppfsc  28532  fnejoin2  28543  upixp  28576  filbcmb  28587  sstotbnd2  28626  isbnd3  28636  prdsbnd2  28647  cntotbnd  28648  ismtyima  28655  bfp  28676  rrncmslem  28684  unichnidl  28784  nacsfix  29001  mzpsubst  29038  mzpcompact2lem  29041  eldioph2lem2  29052  eldioph2  29053  eldioph2b  29054  diophin  29064  diophun  29065  irrapxlem3  29118  irrapxlem5  29120  pell1234qrreccl  29148  pell1234qrmulcl  29149  pell14qrdich  29163  pell1qrge1  29164  pell1qrgaplem  29167  monotuz  29235  rpexpmord  29242  acongtr  29274  acongrep  29276  jm2.23  29298  jm2.26a  29302  jm2.26lem3  29303  jm2.26  29304  jm2.27  29310  wepwsolem  29347  fnwe2lem2  29357  kelac1  29369  kercvrlsm  29389  hbtlem5  29437  hbt  29439  mpaaeu  29460  cncmpmax  29707  rfcnnnub  29711  stoweidlem31  29779  stoweidlem34  29782  stoweidlem35  29783  stoweidlem49  29797  stoweidlem59  29807  stoweidlem62  29810  modfsummod  30198  reuccats1  30214  usg2spthonot1  30362  wwlkext2clwwlk  30418  usgfidegfi  30480  usg2spot2nb  30611  numclwwlk6  30659  mndpsuppss  30735  scmsuppss  30736  dmatsubcl  30800  dmatmulcl  30802  scmatmulcl  30809  pmatcollpw1  30819  lindslinindsimp2lem5  30885  lshpcmp  32473  islshpat  32502  lfl0f  32554  ishlat3N  32839  3dim1  32951  islvol5  33063  lvoli2  33065  lncvrelatN  33265  pclfinclN  33434  pexmidlem8N  33461  idltrn  33634  cdleme42keg  33970  cdleme42mgN  33972  cdlemf2  34046  cdlemg2cex  34075  trlcoat  34207  dihopelvalcpre  34733  dih1dimatlem  34814  dihjatcclem4  34906  lcfl7N  34986  lcfrlem9  35035  mapdh9a  35275  hdmapglem7  35417
  Copyright terms: Public domain W3C validator