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

Theorem simpllr 758
Description: Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.)
Assertion
Ref Expression
simpllr  |-  ( ( ( ( ph  /\  ps )  /\  ch )  /\  th )  ->  ps )

Proof of Theorem simpllr
StepHypRef Expression
1 simpr 461 . 2  |-  ( (
ph  /\  ps )  ->  ps )
21ad2antrr 725 1  |-  ( ( ( ( ph  /\  ps )  /\  ch )  /\  th )  ->  ps )
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:  simp-4r  766  soisoi  6118  f1o2ndf1  6780  tfrlem1  6935  tz7.49  7000  omabs  7186  omxpenlem  7512  fopwdom  7519  findcard3  7656  frfi  7658  finsschain  7719  marypha1lem  7784  wdomtr  7891  cantnfp1  7990  cantnfp1OLD  8016  harcard  8249  numacn  8320  infunsdom1  8483  cofsmo  8539  sornom  8547  ssfin4  8580  fin1a2lem11  8680  fin1a2lem13  8682  ttukeylem5  8783  fpwwe2lem13  8910  pwfseq  8932  00id  9645  addid1  9650  cnegex  9651  negeu  9701  add20  9952  ltmul12a  10286  lediv12a  10326  cru  10415  qextltlem  11273  xleadd1a  11317  xmullem  11328  xlemul1a  11352  ixxss12  11421  ioodisj  11516  seqf1o  11948  mulexpz  12005  leexp1a  12023  faclbnd  12167  swrdswrdlem  12455  abs3lem  12928  cau3lem  12944  rlim3  13078  ello12  13096  lo1bdd2  13104  elo12  13107  rlimconst  13124  isercoll  13247  climcau  13250  climbdd  13251  summolem2  13295  fsumconst  13359  o1fsum  13378  incexclem  13401  bitsfzo  13733  dvdsmulgcd  13840  pc2dvds  14047  pcz  14049  pcadd  14053  pcfac  14063  vdwmc2  14142  vdwlem2  14145  vdwlem10  14153  vdw  14157  ramcl  14192  sbcie3s  14320  firest  14473  prdsval  14495  mreexd  14682  mreexexlemd  14684  iscat  14712  cidfval  14716  iscatd2  14721  catcocl  14725  catass  14726  catpropd  14750  cidpropd  14751  moni  14777  monpropd  14778  issubc  14850  subccocl  14857  funcco  14883  funcpropd  14912  fullpropd  14932  nati  14967  natpropd  14988  fucpropd  14989  xpcpropd  15120  curfuncf  15150  curf2ndf  15159  yonffthlem  15194  acsfiindd  15449  mndpropd  15548  mhmeql  15594  isgrpinv  15690  conjnmzb  15883  gass  15921  symgextf  16024  dfod2  16169  gexdvds  16187  sylow3lem2  16231  efgredlem  16348  efgredeu  16353  oddvdssubg  16441  dprdfcntz  16604  dprdfcntzOLD  16610  pgpfaclem3  16689  issrg  16714  isrng  16755  dvdsrmul1  16851  issubdrg  16996  islmhm2  17225  lmhmeql  17242  lssacsex  17331  issubassa2  17521  opsrval  17663  isphl  18166  uvcf1  18326  lindfmm  18365  mdetunilem7  18540  gsummatr01lem4  18580  cctop  18726  neiptoptop  18851  neiptopreu  18853  tgrest  18879  ordtrest2lem  18923  cnss1  18996  cncnp  19000  isnrm3  19079  uncmp  19122  cmpfi  19127  iuncon  19148  1stcrest  19173  subislly  19201  islly2  19204  cldllycmp  19215  lly1stc  19216  llycmpkgen2  19239  kgencn  19245  xkoccn  19308  ptcnplem  19310  pthaus  19327  txhaus  19336  txkgen  19341  xkohaus  19342  xkococnlem  19348  txcon  19378  regr1lem2  19429  kqreglem1  19430  reghmph  19482  nrmhmph  19483  trfil2  19576  ufileu  19608  flimopn  19664  flimcf  19671  fclscf  19714  ufilcmp  19721  cnpfcf  19730  cnextfun  19752  tgpmulg  19780  symgtgp  19788  tgpt0  19805  divstgplem  19807  ustex2sym  19907  ustex3sym  19908  trust  19920  restutop  19928  restutopopn  19929  ustuqtop2  19933  ustuqtop4  19935  utop3cls  19942  utopreg  19943  cstucnd  19975  ucncn  19976  trcfilu  19985  neipcfilu  19987  ismet2  20024  metequiv2  20201  metcnp  20232  metcnp2  20233  metcnpi3  20237  txmetcnp  20238  metusttoOLD  20248  metustto  20249  metustsymOLD  20252  metustsym  20253  metustOLD  20258  metust  20259  cfilucfilOLD  20260  cfilucfil  20261  metuel2  20270  metutopOLD  20273  psmetutop  20274  restmetu  20278  metucnOLD  20279  metucn  20280  ngptgp  20338  tngngp  20356  nmoleub  20426  icccmp  20518  reconnlem2  20520  reconn  20521  xmetdcn2  20530  metdseq0  20546  metdscn  20548  elcncf2  20582  cncfmet  20600  cnheibor  20643  nmoleub2lem2  20787  nmoleub3  20790  iscfil2  20893  iscfil3  20900  cfilfcls  20901  equivcfil  20926  caubl  20934  bcthlem5  20955  pmltpc  21050  ovollb2  21088  ovoliunnul  21106  ovolicc2lem4  21119  volsup  21153  ioorf  21169  dyadss  21190  dyaddisjlem  21191  mbfposr  21246  cncombf  21252  mbflimsup  21260  i1fmulclem  21296  mbfi1fseqlem4  21312  iblss2  21399  ellimc2  21468  ellimc3  21470  dvnadd  21519  dvmptfsum  21563  dvferm1  21573  dvferm2  21575  fta1g  21755  plyeq0lem  21794  plydivex  21879  fta1  21890  aalioulem2  21915  aalioulem3  21916  ulmuni  21973  ulmbdd  21979  ulmdvlem3  21983  mtest  21985  abelthlem8  22020  pilem3  22034  efopn  22219  cxpmul2z  22252  cxpcn3lem  22301  jensen  22498  isppw2  22569  sqf11  22593  mersenne  22682  dchrelbas3  22693  dchrptlem1  22719  dchrpt  22722  lgsval2lem  22761  lgsdchrval  22802  lgsquad3  22816  2sqb  22833  pntrsumbnd2  22932  pntpbnd  22953  pntibnd  22958  istrkgc  23031  istrkgb  23032  tglowdim1i  23072  tgbtwndiff  23077  tgifscgr  23080  tgcgrxfr  23089  lnext  23119  tgbtwnconn1lem3  23126  tgbtwnconn1  23127  legval  23136  legov  23137  legov2  23138  legtrd  23141  legtri3  23142  tglnne  23156  tglndim0  23157  tglinethru  23164  tglnpt2  23168  colline  23177  tglowdim2l  23178  tglowdim2ln  23179  mirreu3  23184  miriso  23199  midexlem  23212  isperp  23231  perpcom  23232  perpneq  23233  isperp2  23234  footex  23237  colperplem3  23242  mideulem  23244  mideu  23245  f1otrg  23252  f1otrge  23253  axsegcon  23308  axeuclidlem  23343  axcontlem2  23346  usgra1  23427  usgrares1  23458  nbgraf1olem5  23489  pthdepisspth  23608  iseupa  23721  eupath2  23736  isgrp2d  23857  smcnlem  24227  0lno  24325  ubthlem1  24406  ubthlem3  24408  chocunii  24839  occl  24842  5oalem1  25192  3oalem2  25201  nmopub2tALT  25448  nmfnleub2  25465  lnconi  25572  kbass5  25659  mdslmd1lem1  25864  mdslmd1lem2  25865  cdj1i  25972  disjabrex  26060  disjabrexf  26061  fgreu  26124  xrge0infss  26187  xrofsup  26189  ressprs  26250  xrge0addgt0  26288  submarchi  26337  isarchi3  26338  archiabllem1  26344  archiabllem2a  26345  gsumle  26380  suborng  26417  isarchiofld  26419  pstmxmet  26458  sqsscirc1  26472  ordtrest2NEWlem  26486  ordtconlem1  26488  pnfneige0  26515  lmxrge0  26516  lmdvg  26517  qqhval2  26545  esumcst  26648  esumfsup  26653  esumcvg  26669  sigaclfu2  26698  insiga  26714  measinb  26769  imambfm  26811  oms0  26844  eulerpartlemgvv  26893  dstrvprob  26988  sgnmul  27059  sgnsub  27061  signstfvneq0  27107  afsval  27129  lgambdd  27157  lgamucov  27158  derangenlem  27193  sconpi1  27262  cvmsss2  27297  cvmopnlem  27301  cvmlift3lem7  27348  fprodconst  27623  ifscgr  28209  cgrxfr  28220  btwnconn1lem13  28264  outsideofeu  28296  heicant  28564  mblfinlem1  28566  itg2addnclem  28581  ftc1cnnc  28604  ftc1anclem7  28611  neibastop2lem  28719  sstotbnd2  28811  equivtotbnd  28815  isbnd3  28821  ssbnd  28825  totbndbnd  28826  cntotbnd  28833  heibor1lem  28846  rrncmslem  28869  mzpindd  29220  mzpsubst  29223  mzpcompact2lem  29226  eldioph2b  29239  irrapxlem3  29303  irrapxlem5  29305  pellex  29314  pell1234qrdich  29340  pell14qrexpcl  29346  congabseq  29455  jm2.26a  29487  jm2.26lem3  29488  rmydioph  29501  lnrfg  29613  hbt  29624  fnchoice  29889  cncmpmax  29892  climrec  29914  climsuse  29919  stoweidlem7  29940  stoweidlem34  29967  stoweidlem52  29985  stoweidlem60  29993  wallispilem3  30000  usgra2pthspth  30433  el2spthonot  30527  usg2wotspth  30541  clwwlkf1  30596  Lemma2  30631  frgrancvvdeqlem9  30772  friendshipgt3  30852  fsuppmapnn0fz  30935  lindslinindsimp2  31104  snlindsntor  31112  lincresunit2  31119  islindeps2  31124  m2cpmfo  31215  pmatcollpw1dst  31228  pmatcollpw4fi1lem1  31242  mp2pm2mplem4  31264  pmattomply1ghm  31270  chfacfscmulfsupp  31313  chfacfpmmulfsupp  31317  4animp1  31501  4an4132  31503  iunconlem2  31971  lssats  32963  lsat0cv  32984  lkrlss  33046  lfl1dim  33072  lfl1dim2N  33073  lkrpssN  33114  hlhgt2  33339  3dim2  33418  2dim  33420  lplncvrlvol  33566  paddasslem11  33780  pmapjat1  33803  2polssN  33865  pclfinclN  33900  pexmidlem8N  33927  lhpexle1lem  33957  4atex  34026  ltrnid  34085  trlator0  34121  cdlemg2cex  34541  tendodi1  34734  tendodi2  34735  diblss  35121  dihopelvalcpre  35199  dihatexv  35289  mapdval4N  35583
  Copyright terms: Public domain W3C validator