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  6196  soisoi  6234  f1o2ndf1  6915  tz7.49  7170  omabs  7356  omxpenlem  7679  fopwdom  7686  findcard3  7820  frfi  7822  finsschain  7887  marypha1lem  7953  wdomtr  8090  cantnfp1  8185  harcard  8411  numacn  8478  infunsdom1  8641  cofsmo  8697  sornom  8705  ssfin4  8738  fin1a2lem11  8838  fin1a2lem13  8840  ttukeylem5  8941  fpwwe2lem13  9066  pwfseq  9088  mulcmpblnr  9494  00id  9807  addid1  9812  cnegex  9813  negeu  9864  add20  10125  ltmul12a  10460  lediv12a  10499  fiminre  10555  cru  10601  qextltlem  11495  xleadd1a  11539  xmullem  11550  xlemul1a  11574  ixxss12  11655  ioodisj  11760  fsuppmapnn0fz  12205  seqf1o  12251  mulexpz  12309  leexp1a  12328  faclbnd  12472  swrdswrdlem  12800  abs3lem  13380  cau3lem  13396  rlim3  13540  ello12  13558  lo1bdd2  13566  elo12  13569  rlimconst  13586  isercoll  13709  climcau  13712  climbdd  13713  summolem2  13760  fsumconst  13829  o1fsum  13851  incexclem  13872  fprodconst  14010  bitsfzo  14383  dvdsmulgcd  14493  pc2dvds  14782  pcz  14784  pcadd  14788  pcfac  14798  vdwmc2  14883  vdwlem2  14886  vdwlem10  14894  vdw  14898  ramcl  14941  sbcie3s  15121  firest  15281  prdsval  15303  mreexd  15490  mreexexlemd  15492  iscat  15520  cidfval  15524  iscatd2  15529  catcocl  15533  catass  15534  catpropd  15556  cidpropd  15557  moni  15583  monpropd  15584  issubc  15682  subccocl  15692  funcco  15718  funcpropd  15747  fullpropd  15767  nati  15802  natpropd  15823  fucpropd  15824  xpcpropd  16035  curfuncf  16065  curf2ndf  16074  yonffthlem  16109  acsfiindd  16365  mndpropd  16504  mhmeql  16553  isgrpinv  16658  mhmmnd  16750  conjnmzb  16859  gass  16897  symgextf  17000  dfod2  17144  gexdvds  17162  sylow3lem2  17206  efgredlem  17323  efgredeu  17328  ghmcmn  17398  oddvdssubg  17419  dprdfcntz  17574  pgpfaclem3  17642  issrg  17667  isring  17710  dvdsrmul1  17807  issubdrg  17959  islmhm2  18187  lmhmeql  18204  lssacsex  18293  issubassa2  18495  opsrval  18624  isphl  19117  uvcf1  19272  lindfmm  19307  scmatmats  19458  smatvscl  19471  mdetunilem7  19565  gsummatr01lem4  19605  m2cpmfo  19702  decpmatmulsumfsupp  19719  pmatcollpw3fi1lem1  19732  pm2mpf1lem  19740  pm2mpf1  19745  mp2pm2mplem4  19755  pm2mpghm  19762  pm2mpmhmlem1  19764  pm2mpmhmlem2  19765  chfacfscmulfsupp  19805  chfacfpmmulfsupp  19809  cctop  19943  neiptoptop  20069  neiptopreu  20071  tgrest  20097  ordtrest2lem  20141  cnss1  20214  cncnp  20218  isnrm3  20297  uncmp  20340  cmpfi  20345  iuncon  20365  1stcrest  20390  subislly  20418  islly2  20421  cldllycmp  20432  lly1stc  20433  llycmpkgen2  20487  kgencn  20493  xkoccn  20556  ptcnplem  20558  pthaus  20575  txhaus  20584  txkgen  20589  xkohaus  20590  xkococnlem  20596  txcon  20626  regr1lem2  20677  kqreglem1  20678  reghmph  20730  nrmhmph  20731  trfil2  20824  ufileu  20856  flimopn  20912  flimcf  20919  fclscf  20962  ufilcmp  20969  cnpfcf  20978  cnextfun  21001  tgpmulg  21030  symgtgp  21038  tgpt0  21055  qustgplem  21057  ustex2sym  21153  ustex3sym  21154  trust  21166  restutop  21174  restutopopn  21175  ustuqtop2  21179  ustuqtop4  21181  utop3cls  21188  utopreg  21189  cstucnd  21221  ucncn  21222  trcfilu  21231  neipcfilu  21233  ismet2  21270  metequiv2  21447  metcnp  21478  metcnp2  21479  metcnpi3  21483  txmetcnp  21484  metustto  21490  metustsym  21492  metust  21495  cfilucfil  21496  metuel2  21502  psmetutop  21504  restmetu  21507  metucn  21508  ngptgp  21566  tngngp  21584  nmoleub  21654  icccmp  21745  reconnlem2  21747  reconn  21748  xmetdcn2  21757  metdseq0  21773  metdscn  21775  elcncf2  21809  cncfmet  21827  cnheibor  21870  nmoleub2lem2  22014  nmoleub3  22017  iscfil2  22120  iscfil3  22127  cfilfcls  22128  equivcfil  22153  caubl  22161  bcthlem5  22180  pmltpc  22273  ovollb2  22311  ovoliunnul  22329  ovolicc2lem4  22342  volsup  22377  ioorf  22393  ioorfOLD  22398  dyadss  22420  dyaddisjlem  22421  mbfposr  22476  cncombf  22482  mbflimsup  22491  mbflimsupOLD  22492  i1fmulclem  22528  mbfi1fseqlem4  22544  iblss2  22631  ellimc2  22700  ellimc3  22702  dvnadd  22751  dvmptfsum  22795  dvferm1  22805  dvferm2  22807  fta1g  22984  plyeq0lem  23023  plydivex  23109  fta1  23120  aalioulem2  23145  aalioulem3  23146  ulmuni  23203  ulmbdd  23209  ulmdvlem3  23213  mtest  23215  abelthlem8  23250  pilem3  23265  pilem3OLD  23266  efopn  23459  cxpmul2z  23492  cxpcn3lem  23543  jensen  23770  lgambdd  23818  lgamucov  23819  isppw2  23896  sqf11  23920  mersenne  24009  dchrelbas3  24020  dchrptlem1  24046  dchrpt  24049  lgsval2lem  24088  lgsdchrval  24129  lgsquad3  24143  2sqb  24160  pntrsumbnd2  24259  pntpbnd  24280  pntibnd  24285  istrkgc  24356  istrkgb  24357  tglowdim1i  24399  tgbtwndiff  24404  tgifscgr  24407  tgcgrxfr  24416  lnext  24463  tgbtwnconn1lem3  24470  tgbtwnconn1  24471  legval  24480  legov  24481  legov2  24482  legtrd  24485  legtri3  24486  legso  24495  hlcgrex  24511  hlcgreu  24513  tglnne  24523  tglndim0  24524  tglineeltr  24526  tglinethru  24531  tglnne0  24535  tglnpt2  24536  colline  24545  tglowdim2l  24546  tglowdim2ln  24547  mirreu3  24550  miriso  24565  midexlem  24585  isperp  24605  perpcom  24606  perpneq  24607  isperp2  24608  footex  24611  colperpexlem3  24622  opphllem  24625  midex  24627  oppne3  24633  opptgdim2  24635  opphllem2  24638  opphllem3  24639  opphllem5  24641  opphllem6  24642  opphl  24644  outpasch  24645  lnopp2hpgb  24652  colopp  24658  lmieu  24673  trgcopy  24693  trgcopyeu  24695  iscgra1  24699  cgrane1  24701  cgrane2  24702  cgrane3  24703  cgrahl1  24705  cgrahl2  24706  cgracgr  24707  cgraswap  24709  cgracom  24711  cgratr  24712  cgrabtwn  24713  cgrahl  24714  dfcgra2  24717  acopyeu  24719  f1otrg  24738  f1otrge  24739  axsegcon  24794  axeuclidlem  24829  axcontlem2  24832  usgra1  24937  usgrares1  24974  nbgraf1olem5  25009  pthdepisspth  25140  clwwlkf1  25360  clwwlknscsh  25383  el2spthonot  25434  usg2wotspth  25448  iseupa  25529  eupath2  25544  frgrancvvdeqlem9  25605  friendshipgt3  25685  isgrp2d  25799  smcnlem  26169  0lno  26267  ubthlem1  26348  ubthlem3  26350  chocunii  26780  occl  26783  5oalem1  27133  3oalem2  27142  nmopub2tALT  27388  nmfnleub2  27405  lnconi  27512  kbass5  27599  mdslmd1lem1  27804  mdslmd1lem2  27805  cdj1i  27912  disjabrex  28022  disjabrexf  28023  acunirnmpt  28092  acunirnmpt2  28093  acunirnmpt2f  28094  aciunf1lem  28095  fgreu  28105  xrge0infss  28172  xrofsup  28180  2sqmo  28239  ressprs  28245  xrge0addgt0  28283  submarchi  28332  isarchi3  28333  archiabllem1  28339  archiabllem2a  28340  gsumle  28371  suborng  28408  isarchiofld  28410  psgnfzto1stlem  28443  fzto1st1  28445  mdetpmtr1  28479  fimaproj  28490  txomap  28491  qtophaus  28493  cmpcref  28507  pstmxmet  28530  sqsscirc1  28544  ordtrest2NEWlem  28558  ordtconlem1  28560  pnfneige0  28587  lmxrge0  28588  lmdvg  28589  qqhval2  28616  esumcst  28714  esumrnmpt2  28719  esumfsup  28721  esumcvg  28737  esum2d  28744  esumiun  28745  sigaclfu2  28773  insiga  28789  ldsysgenld  28812  ldgenpisyslem1  28815  fiunelros  28826  measinb  28873  imambfm  28914  oms0  28949  omssubadd  28952  carsgclctunlem3  28972  eulerpartlemgvv  29026  dstrvprob  29121  sgnsub  29194  signstfvneq0  29240  afsval  29267  derangenlem  29673  sconpi1  29741  cvmsss2  29776  cvmopnlem  29780  cvmlift3lem7  29827  msrval  29955  ifscgr  30587  cgrxfr  30598  btwnconn1lem13  30642  outsideofeu  30674  neibastop2lem  30792  poimirlem14  31648  poimirlem22  31656  poimirlem29  31663  broucube  31668  heicant  31669  mblfinlem1  31671  itg2addnclem  31687  ftc1cnnc  31710  ftc1anclem7  31717  sstotbnd2  31800  equivtotbnd  31804  isbnd3  31810  ssbnd  31814  totbndbnd  31815  cntotbnd  31822  heibor1lem  31835  rrncmslem  31858  lssats  32277  lsat0cv  32298  lkrlss  32360  lfl1dim  32386  lfl1dim2N  32387  lkrpssN  32428  hlhgt2  32653  3dim2  32732  2dim  32734  lplncvrlvol  32880  paddasslem11  33094  pmapjat1  33117  2polssN  33179  pclfinclN  33214  pexmidlem8N  33241  lhpexle1lem  33271  4atex  33340  ltrnid  33399  trlator0  33436  cdlemg2cex  33857  tendodi1  34050  tendodi2  34051  diblss  34437  dihopelvalcpre  34515  dihatexv  34605  mapdval4N  34899  mzpindd  35287  mzpsubst  35289  mzpcompact2lem  35292  eldioph2b  35304  irrapxlem3  35368  irrapxlem5  35370  pellex  35379  pell1234qrdich  35405  pell14qrexpcl  35411  congabseq  35520  jm2.26a  35551  jm2.26lem3  35552  rmydioph  35565  lnrfg  35674  hbt  35685  4an4132  36482  iunconlem2  36962  fnchoice  36980  cncmpmax  36983  disjf1  37070  supxrge  37160  suplesup  37161  climrec  37243  climsuse  37249  islptre  37261  addlimc  37291  0ellimcdiv  37292  icccncfext  37327  cncfiooicclem1  37333  fperdvper  37352  ioodvbdlimc1lem2  37366  ioodvbdlimc2lem  37368  dvmptfprodlem  37378  dvmptfprod  37379  dvnprodlem2  37381  stoweidlem7  37426  stoweidlem34  37454  stoweidlem52  37472  stoweidlem60  37480  wallispilem3  37488  fourierdlem34  37562  fourierdlem38  37566  fourierdlem39  37567  fourierdlem48  37576  fourierdlem50  37578  fourierdlem51  37579  fourierdlem73  37601  fourierdlem76  37604  fourierdlem77  37605  fourierdlem80  37608  fourierdlem87  37615  fourierdlem103  37631  fourierdlem104  37632  etransclem32  37688  etransclem33  37689  sge0f1o  37748  sge0pr  37760  iundjiun  37797  bgoldbtbndlem2  38281  bgoldbtbndlem3  38282  bgoldbtbnd  38284  usgra2pthspth  38411  mgmhmeql  38551  isrng  38624  2zlidl  38682  lindslinindsimp2  39006  snlindsntor  39014  lincresunit2  39021  islindeps2  39026
  Copyright terms: Public domain W3C validator