MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  simplrr Structured version   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  2684  rmob  3249  disjxiun  4209  isotr  6056  weniso  6075  riota5f  6574  tfrlem9a  6647  oaass  6804  oeeui  6845  oaabs2  6888  resixpfo  7100  omxpenlem  7209  pw2f1olem  7212  fopwdom  7216  fofinf1o  7387  marypha1lem  7438  ordiso2  7484  oismo  7509  ixpiunwdom  7559  cantnf  7649  fseqenlem1  7905  iunfictbso  7995  dfac12lem2  8024  dfac12lem3  8025  infunsdom1  8093  infpssrlem5  8187  fin23lem24  8202  isf32lem2  8234  isf32lem4  8236  isf34lem4  8257  fin1a2lem12  8291  fin1a2lem13  8292  ttukeylem6  8394  fpwwe2lem12  8516  fpwwe2lem13  8517  fpwwe2  8518  winalim2  8571  wunex2  8613  tskord  8655  prlem934  8910  addid1  9246  cnegex  9247  negeu  9296  add20  9540  divdivdiv  9715  ltmul12a  9866  lemul12a  9868  lediv12a  9903  supmul1  9973  cru  9992  uzwo3  10569  xleadd1a  10832  xmullem  10843  xmulgt0  10862  xlemul1a  10867  ixxun  10932  ixxss12  10936  ioodisj  11026  mulexpz  11420  leexp1a  11438  expmulnbnd  11511  hashf1  11706  brfi1uzind  11715  abs3lem  12142  rexanre  12150  cau3lem  12158  limsupgre  12275  limsupbnd2  12277  o1lo1  12331  rlimclim1  12339  rlimclim  12340  rlimcn1  12382  rlimcn2  12384  o1of2  12406  o1rlimmul  12412  lo1add  12420  lo1mul  12421  isercolllem1  12458  climcau  12464  caucvgrlem  12466  caucvgb  12473  summolem2  12510  summo  12511  o1fsum  12592  isprm6  13109  isprm5  13112  rpdvds  13124  pclem  13212  pcqmul  13227  pcexp  13233  pcneg  13247  pcprmpw2  13255  pcadd  13258  pcmpt  13261  4sqlem13  13325  vdwlem2  13350  vdwlem7  13355  vdwlem12  13360  ramval  13376  ramub2  13382  ramz2  13392  ramcl  13397  imasval  13737  imasdsval  13741  mreexexd  13873  acsfn  13884  issubc3  14046  idfucl  14078  funcres2c  14098  isnat  14144  fucpropd  14174  xpcval  14274  xpcco  14280  prfval  14296  evlf2  14315  evlfcl  14319  curf12  14324  curf1cl  14325  curf2  14326  curfcl  14329  curf2ndf  14344  hof2val  14353  hofcl  14356  hofpropd  14364  yonedalem4a  14372  yonedainv  14378  drsdirfi  14395  pospo  14430  poslubmo  14573  isipodrs  14587  acsinfd  14606  mndpropd  14721  mhmeql  14764  gsumvalx  14774  frmdup3  14811  issubg4  14961  ssnmz  14982  conjnmzb  15040  pgpfi  15239  sylow2blem3  15256  slwhash  15258  fislw  15259  sylow3lem2  15262  lsmdisj2  15314  pj1eu  15328  efgredlem  15379  frgpuplem  15404  gexex  15468  frgpnabl  15486  dprdfadd  15578  dpjidcl  15616  pgpfac1lem3  15635  pgpfaclem3  15641  ablfac2  15647  rngpropd  15695  islmhm2  16114  lmhmpropd  16145  lbsextlem4  16233  assapropd  16386  psrval  16429  prmirredlem  16773  lsmcss  16919  pptbas  17072  toponmre  17157  restbas  17222  iscncl  17333  cnrest2  17350  cnpdis  17357  lmcnp  17368  dishaus  17446  cmpcovf  17454  tgcmp  17464  dfcon2  17482  clscon  17493  2ndcctbss  17518  dis2ndc  17523  1stccnp  17525  islly2  17547  cldllycmp  17558  kgentopon  17570  txcls  17636  ptpjopn  17644  dfac14  17650  xkoccn  17651  txcnp  17652  txcmpb  17676  txlm  17680  xkopt  17687  xkoco1cn  17689  xkoco2cn  17690  qtopcn  17746  qtoprest  17749  regr1lem2  17772  xkocnv  17846  qtophmeo  17849  fmfnfmlem4  17989  hausflim  18013  hauspwpwf1  18019  fclscmp  18062  alexsublem  18075  alexsubALTlem2  18079  alexsubALTlem3  18080  ptcmplem3  18085  ptcmplem4  18086  ptcmplem5  18087  cnextfun  18095  tmdgsum2  18126  symgtgp  18131  tsmsval2  18159  tsmsgsum  18168  utoptop  18264  ismet2  18363  blin  18451  metss2lem  18541  methaus  18550  met1stc  18551  met2ndci  18552  prdsxmslem2  18559  metcnp3  18570  metcnpi3  18576  metusttoOLD  18587  metustto  18588  metustfbasOLD  18595  metustfbas  18596  nlmvscn  18723  nrginvrcn  18727  xrsxmet  18840  reconnlem1  18857  reconn  18859  xrge0tsms  18865  xmetdcn2  18868  metdscn  18886  addcnlem  18894  fsumcn  18900  cnheiborlem  18979  cnheibor  18980  bndth  18983  lebnum  18989  nmoleub2lem2  19124  ipcn  19200  iscmet3  19246  caubl  19260  minveclem3b  19329  minveclem7  19336  pjthlem2  19339  pmltpc  19347  volfiniun  19441  ioombl1  19456  dyadss  19486  dyaddisjlem  19487  dyadmax  19490  dyadmbllem  19491  opnmbllem  19493  itg1addlem2  19589  itg10a  19602  mbfi1fseqlem6  19612  itg2seq  19634  itg2monolem1  19642  itg2gt0  19652  itgfsum  19718  limcfval  19759  ellimc2  19764  ellimc3  19766  limcres  19773  limciun  19781  dvres  19798  dveflem  19863  rolle  19874  dvlip2  19879  c1liplem1  19880  dvgt0lem1  19886  dvgt0  19888  dvlt0  19889  dvne0  19895  dvfsumrlimge0  19914  ftc1lem6  19925  itgsubst  19933  evlslem1  19936  mdegmullem  20001  ply1domn  20046  ply1divex  20059  fta1g  20090  fta1b  20092  plyf  20117  dgrlem  20148  coeid  20157  plydivalg  20216  aannenlem1  20245  aalioulem3  20251  aalioulem6  20254  abelthlem8  20355  efif1olem4  20447  chordthm  20678  xrlimcnp  20807  jensen  20827  sqf11  20922  fsumvma2  20998  perfectlem2  21014  lgsdilem  21106  lgsquad2lem2  21143  lgsquad3  21145  2sqlem5  21152  2sqlem9  21157  2sqb  21162  rpvmasumlem  21181  dchrisum0flb  21204  dchrisum0  21214  pntpbnd  21282  pntibndlem3  21286  pntleml  21305  cusgrarn  21468  usgrasscusgra  21492  4cycl4dv4e  21655  eupath2  21702  vacn  22190  blocni  22306  ubthlem3  22374  minvecolem7  22385  chocunii  22803  pjhthmo  22804  pjhthlem2  22894  kbass5  23623  mdsymlem5  23910  xrofsup  24126  gsumpropd2lem  24220  xrge0tsmsd  24223  qqhval2  24366  volmeas  24587  ballotlemfc0  24750  ballotlemfcc  24751  lgamcvglem  24824  lgamcvg2  24839  derangenlem  24857  erdsze2lem1  24889  pconcon  24918  conpcon  24922  cvxscon  24930  cvmliftmolem2  24969  cvmliftmo  24971  cvmlift2lem10  24999  cvmlift2lem12  25001  cvmlift3lem7  25012  dedekind  25187  prodmolem2  25261  poseq  25528  brcgr  25839  brbtwn2  25844  colinearalg  25849  axsegcon  25866  axeuclidlem  25901  axcontlem9  25911  ifscgr  25978  cgrxfr  25989  btwnconn1lem13  26033  btwnconn1lem14  26034  outsideofeq  26064  ellines  26086  supaddc  26237  opnmbllem0  26242  mblfinlem3  26245  itg2addnclem  26256  itg2addnc  26259  ftc1cnnc  26279  finminlem  26321  locfincmp  26384  comppfsc  26387  fnejoin2  26398  upixp  26431  filbcmb  26442  sstotbnd2  26483  isbnd3  26493  prdsbnd2  26504  cntotbnd  26505  ismtyima  26512  bfp  26533  rrncmslem  26541  unichnidl  26641  nacsfix  26766  mzpsubst  26805  mzpcompact2lem  26808  eldioph2lem2  26819  eldioph2  26820  eldioph2b  26821  diophin  26831  diophun  26832  irrapxlem3  26887  irrapxlem5  26889  pell1234qrreccl  26917  pell1234qrmulcl  26918  pell14qrdich  26932  pell1qrge1  26933  pell1qrgaplem  26936  monotuz  27004  rpexpmord  27011  acongtr  27043  acongrep  27045  jm2.23  27067  jm2.26a  27071  jm2.26lem3  27072  jm2.26  27073  jm2.27  27079  wepwsolem  27116  fnwe2lem2  27126  kelac1  27138  kercvrlsm  27158  uvcf1  27218  frlmsslsp  27225  frlmup1  27227  hbtlem5  27309  hbt  27311  mpaaeu  27332  f1otrspeq  27367  psgneu  27406  mamucl  27433  mamulid  27435  mamurid  27436  mamuass  27437  mamudi  27438  mamudir  27439  mamuvs1  27440  mamuvs2  27441  cncmpmax  27679  rfcnnnub  27683  stoweidlem31  27756  stoweidlem34  27759  stoweidlem35  27760  stoweidlem49  27774  stoweidlem59  27784  stoweidlem62  27787  fz0fzelfz0  28118  cshweqdif2s  28271  cshwssizelem4a  28283  usg2spthonot1  28357  usgfidegfi  28360  usg2spot2nb  28454  lshpcmp  29786  islshpat  29815  lfl0f  29867  ishlat3N  30152  3dim1  30264  islvol5  30376  lvoli2  30378  lncvrelatN  30578  pclfinclN  30747  pexmidlem8N  30774  idltrn  30947  cdleme42keg  31283  cdleme42mgN  31285  cdlemf2  31359  cdlemg2cex  31388  trlcoat  31520  dihopelvalcpre  32046  dih1dimatlem  32127  dihjatcclem4  32219  lcfl7N  32299  lcfrlem9  32348  mapdh9a  32588  hdmapglem7  32730
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