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

Theorem simpllr 767
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 462 . 2  |-  ( (
ph  /\  ps )  ->  ps )
21ad2antrr 730 1  |-  ( ( ( ( ph  /\  ps )  /\  ch )  /\  th )  ->  ps )
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:  simp-4r  775  fsnex  6135  soisoi  6173  f1o2ndf1  6854  tz7.49  7112  omabs  7298  omxpenlem  7621  fopwdom  7628  findcard3  7762  frfi  7764  finsschain  7829  marypha1lem  7895  wdomtr  8038  cantnfp1  8133  harcard  8359  numacn  8426  infunsdom1  8589  cofsmo  8645  sornom  8653  ssfin4  8686  fin1a2lem11  8786  fin1a2lem13  8788  ttukeylem5  8889  fpwwe2lem13  9013  pwfseq  9035  mulcmpblnr  9441  00id  9754  addid1  9759  cnegex  9760  negeu  9811  add20  10072  ltmul12a  10407  lediv12a  10445  fiminre  10501  cru  10547  qextltlem  11441  xleadd1a  11485  xmullem  11496  xlemul1a  11520  ixxss12  11601  ioodisj  11708  fsuppmapnn0fz  12153  seqf1o  12199  mulexpz  12257  leexp1a  12276  faclbnd  12420  swrdswrdlem  12756  abs3lem  13340  cau3lem  13356  rlim3  13500  ello12  13518  lo1bdd2  13526  elo12  13529  rlimconst  13546  isercoll  13669  climcau  13672  climbdd  13673  summolem2  13720  fsumconst  13789  o1fsum  13811  incexclem  13832  fprodconst  13970  bitsfzo  14347  dvdsmulgcd  14460  pc2dvds  14766  pcz  14768  pcadd  14772  pcfac  14782  vdwmc2  14867  vdwlem2  14870  vdwlem10  14878  vdw  14882  ramcl  14925  sbcie3s  15105  firest  15269  prdsval  15291  mreexd  15486  mreexexlemd  15488  iscat  15516  cidfval  15520  iscatd2  15525  catcocl  15529  catass  15530  catpropd  15552  cidpropd  15553  moni  15579  monpropd  15580  issubc  15678  subccocl  15688  funcco  15714  funcpropd  15743  fullpropd  15763  nati  15798  natpropd  15819  fucpropd  15820  xpcpropd  16031  curfuncf  16061  curf2ndf  16070  yonffthlem  16105  acsfiindd  16361  mndpropd  16500  mhmeql  16549  isgrpinv  16654  mhmmnd  16746  conjnmzb  16855  gass  16893  symgextf  16996  dfod2  17153  gexdvds  17173  sylow3lem2  17218  efgredlem  17335  efgredeu  17340  ghmcmn  17410  oddvdssubg  17431  dprdfcntz  17586  pgpfaclem3  17654  issrg  17679  isring  17722  dvdsrmul1  17819  issubdrg  17971  islmhm2  18199  lmhmeql  18216  lssacsex  18305  issubassa2  18507  opsrval  18636  isphl  19132  uvcf1  19287  lindfmm  19322  scmatmats  19473  smatvscl  19486  mdetunilem7  19580  gsummatr01lem4  19620  m2cpmfo  19717  decpmatmulsumfsupp  19734  pmatcollpw3fi1lem1  19747  pm2mpf1lem  19755  pm2mpf1  19760  mp2pm2mplem4  19770  pm2mpghm  19777  pm2mpmhmlem1  19779  pm2mpmhmlem2  19780  chfacfscmulfsupp  19820  chfacfpmmulfsupp  19824  cctop  19958  neiptoptop  20084  neiptopreu  20086  tgrest  20112  ordtrest2lem  20156  cnss1  20229  cncnp  20233  isnrm3  20312  uncmp  20355  cmpfi  20360  iuncon  20380  1stcrest  20405  subislly  20433  islly2  20436  cldllycmp  20447  lly1stc  20448  llycmpkgen2  20502  kgencn  20508  xkoccn  20571  ptcnplem  20573  pthaus  20590  txhaus  20599  txkgen  20604  xkohaus  20605  xkococnlem  20611  txcon  20641  regr1lem2  20692  kqreglem1  20693  reghmph  20745  nrmhmph  20746  trfil2  20839  ufileu  20871  flimopn  20927  flimcf  20934  fclscf  20977  ufilcmp  20984  cnpfcf  20993  cnextfun  21016  tgpmulg  21045  symgtgp  21053  tgpt0  21070  qustgplem  21072  ustex2sym  21168  ustex3sym  21169  trust  21181  restutop  21189  restutopopn  21190  ustuqtop2  21194  ustuqtop4  21196  utop3cls  21203  utopreg  21204  cstucnd  21236  ucncn  21237  trcfilu  21246  neipcfilu  21248  ismet2  21285  metequiv2  21462  metcnp  21493  metcnp2  21494  metcnpi3  21498  txmetcnp  21499  metustto  21505  metustsym  21507  metust  21510  cfilucfil  21511  metuel2  21517  psmetutop  21519  restmetu  21522  metucn  21523  ngptgp  21581  tngngp  21599  nmoleub  21673  nmoleubOLD  21689  icccmp  21780  reconnlem2  21782  reconn  21783  xmetdcn2  21792  metdseq0  21808  metdscn  21810  metdseq0OLD  21823  metdscnOLD  21825  elcncf2  21859  cncfmet  21877  cnheibor  21920  nmoleub2lem2  22067  nmoleub3  22070  iscfil2  22173  iscfil3  22180  cfilfcls  22181  equivcfil  22206  caubl  22214  bcthlem5  22233  pmltpc  22338  ovollb2  22379  ovoliunnul  22397  ovolicc2lem4OLD  22410  ovolicc2lem4  22411  volsup  22446  ioorf  22462  ioorfOLD  22467  dyadss  22489  dyaddisjlem  22490  mbfposr  22545  cncombf  22551  mbflimsup  22560  mbflimsupOLD  22561  i1fmulclem  22597  mbfi1fseqlem4  22613  iblss2  22700  ellimc2  22769  ellimc3  22771  dvnadd  22820  dvmptfsum  22864  dvferm1  22874  dvferm2  22876  fta1g  23055  plyeq0lem  23101  plydivex  23187  fta1  23198  aalioulem2  23226  aalioulem3  23227  ulmuni  23284  ulmbdd  23290  ulmdvlem3  23294  mtest  23296  abelthlem8  23331  pilem3  23346  pilem3OLD  23347  efopn  23540  cxpmul2z  23573  cxpcn3lem  23624  jensen  23851  lgambdd  23899  lgamucov  23900  isppw2  23979  sqf11  24003  mersenne  24092  dchrelbas3  24103  dchrptlem1  24129  dchrpt  24132  lgsval2lem  24171  lgsdchrval  24212  lgsquad3  24226  2sqb  24243  pntrsumbnd2  24342  pntpbnd  24363  pntibnd  24368  istrkgc  24439  istrkgb  24440  tglowdim1i  24482  tgbtwndiff  24487  tgifscgr  24490  iscgrglt  24496  tgcgrxfr  24500  lnext  24549  tgbtwnconn1lem3  24556  tgbtwnconn1  24557  legval  24566  legov  24567  legov2  24568  legtrd  24571  legtri3  24572  legso  24581  hlcgrex  24598  hlcgreu  24600  tglnne  24610  tglndim0  24611  tglineeltr  24613  tglinethru  24618  tglnne0  24622  tglnpt2  24623  colline  24631  tglowdim2l  24632  tglowdim2ln  24633  mirreu3  24636  miriso  24652  midexlem  24674  isperp  24694  perpcom  24695  perpneq  24696  isperp2  24697  footex  24700  colperpexlem3  24711  opphllem  24714  midex  24716  oppne3  24722  opptgdim2  24724  opphllem2  24727  opphllem3  24728  opphllem5  24730  opphllem6  24731  opphl  24733  outpasch  24734  lnopp2hpgb  24742  colopp  24748  lmieu  24763  trgcopy  24783  trgcopyeu  24785  iscgra1  24789  cgrane1  24791  cgrane2  24792  cgrane3  24793  cgrahl1  24795  cgrahl2  24796  cgracgr  24797  cgraswap  24799  cgracom  24801  cgratr  24802  cgrabtwn  24804  cgrahl  24805  dfcgra2  24808  sacgr  24809  acopyeu  24812  inaghl  24818  cgrg3col4  24821  f1otrg  24838  f1otrge  24839  axsegcon  24894  axeuclidlem  24929  axcontlem2  24932  usgra1  25037  usgrares1  25075  nbgraf1olem5  25110  pthdepisspth  25241  clwwlkf1  25461  clwwlknscsh  25484  el2spthonot  25535  usg2wotspth  25549  iseupa  25630  eupath2  25645  frgrancvvdeqlem9  25706  friendshipgt3  25786  isgrp2d  25900  smcnlem  26270  0lno  26368  ubthlem1  26449  ubthlem3  26451  chocunii  26891  occl  26894  5oalem1  27244  3oalem2  27253  nmopub2tALT  27499  nmfnleub2  27516  lnconi  27623  kbass5  27710  mdslmd1lem1  27915  mdslmd1lem2  27916  cdj1i  28023  disjabrex  28133  disjabrexf  28134  acunirnmpt  28202  acunirnmpt2  28203  acunirnmpt2f  28204  aciunf1lem  28205  fgreu  28215  xrge0infss  28285  xrge0infssOLD  28286  xrofsup  28298  2sqmo  28356  ressprs  28362  xrge0addgt0  28400  submarchi  28449  isarchi3  28450  archiabllem1  28456  archiabllem2a  28457  gsumle  28488  suborng  28525  isarchiofld  28527  psgnfzto1stlem  28560  fzto1st1  28562  mdetpmtr1  28596  fimaproj  28607  txomap  28608  qtophaus  28610  cmpcref  28624  pstmxmet  28647  sqsscirc1  28661  ordtrest2NEWlem  28675  ordtconlem1  28677  pnfneige0  28704  lmxrge0  28705  lmdvg  28706  qqhval2  28733  esumcst  28831  esumrnmpt2  28836  esumfsup  28838  esumcvg  28854  esum2d  28861  esumiun  28862  sigaclfu2  28890  insiga  28906  ldsysgenld  28929  ldgenpisyslem1  28932  fiunelros  28943  measinb  28990  imambfm  29031  oms0  29072  omssubadd  29075  oms0OLD  29076  omssubaddOLD  29079  carsgclctunlem3  29099  eulerpartlemgvv  29156  dstrvprob  29251  sgnsub  29362  signstfvneq0  29408  afsval  29435  derangenlem  29841  sconpi1  29909  cvmsss2  29944  cvmopnlem  29948  cvmlift3lem7  29995  msrval  30123  ifscgr  30755  cgrxfr  30766  btwnconn1lem13  30810  outsideofeu  30842  neibastop2lem  30960  poimirlem14  31861  poimirlem22  31869  poimirlem29  31876  broucube  31881  heicant  31882  mblfinlem1  31884  itg2addnclem  31900  ftc1cnnc  31923  ftc1anclem7  31930  sstotbnd2  32013  equivtotbnd  32017  isbnd3  32023  ssbnd  32027  totbndbnd  32028  cntotbnd  32035  heibor1lem  32048  rrncmslem  32071  lssats  32490  lsat0cv  32511  lkrlss  32573  lfl1dim  32599  lfl1dim2N  32600  lkrpssN  32641  hlhgt2  32866  3dim2  32945  2dim  32947  lplncvrlvol  33093  paddasslem11  33307  pmapjat1  33330  2polssN  33392  pclfinclN  33427  pexmidlem8N  33454  lhpexle1lem  33484  4atex  33553  ltrnid  33612  trlator0  33649  cdlemg2cex  34070  tendodi1  34263  tendodi2  34264  diblss  34650  dihopelvalcpre  34728  dihatexv  34818  mapdval4N  35112  mzpindd  35500  mzpsubst  35502  mzpcompact2lem  35505  eldioph2b  35517  irrapxlem3  35581  irrapxlem5  35583  pellex  35592  pell1234qrdich  35620  pell14qrexpcl  35626  congabseq  35737  jm2.26a  35768  jm2.26lem3  35769  rmydioph  35782  lnrfg  35891  hbt  35902  4an4132  36768  iunconlem2  37248  fnchoice  37266  cncmpmax  37269  disjf1  37361  supxrge  37458  suplesup  37459  climrec  37564  climsuse  37570  islptre  37582  addlimc  37612  0ellimcdiv  37613  icccncfext  37648  cncfiooicclem1  37654  fperdvper  37673  ioodvbdlimc1lem2  37687  ioodvbdlimc1lem2OLD  37689  ioodvbdlimc2lem  37691  ioodvbdlimc2lemOLD  37692  dvmptfprodlem  37702  dvmptfprod  37703  dvnprodlem2  37705  stoweidlem7  37750  stoweidlem34  37778  stoweidlem52  37796  stoweidlem60  37804  wallispilem3  37812  fourierdlem34  37887  fourierdlem38  37891  fourierdlem39  37892  fourierdlem48  37901  fourierdlem50  37903  fourierdlem51  37904  fourierdlem73  37926  fourierdlem76  37929  fourierdlem77  37930  fourierdlem80  37933  fourierdlem87  37940  fourierdlem103  37956  fourierdlem104  37957  etransclem32  38014  etransclem33  38015  sge0f1o  38075  sge0pr  38087  sge0isum  38120  iundjiun  38149  bgoldbtbndlem2  38714  bgoldbtbndlem3  38715  bgoldbtbnd  38717  upgr1opALT  38975  usgr1eop  39067  usgra2pthspth  39256  mgmhmeql  39394  isrng  39467  2zlidl  39525  lindslinindsimp2  39849  snlindsntor  39857  lincresunit2  39864  islindeps2  39869
  Copyright terms: Public domain W3C validator