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

Theorem simpllr 774
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 467 . 2  |-  ( (
ph  /\  ps )  ->  ps )
21ad2antrr 737 1  |-  ( ( ( ( ph  /\  ps )  /\  ch )  /\  th )  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 375
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 190  df-an 377
This theorem is referenced by:  simp-4r  782  fsnex  6206  soisoi  6244  f1o2ndf1  6931  tz7.49  7188  omabs  7374  omxpenlem  7699  fopwdom  7706  findcard3  7840  frfi  7842  finsschain  7907  marypha1lem  7973  wdomtr  8116  cantnfp1  8212  harcard  8438  numacn  8506  infunsdom1  8669  cofsmo  8725  sornom  8733  ssfin4  8766  fin1a2lem11  8866  fin1a2lem13  8868  ttukeylem5  8969  fpwwe2lem13  9093  pwfseq  9115  mulcmpblnr  9521  00id  9834  addid1  9839  cnegex  9840  negeu  9891  add20  10154  ltmul12a  10489  lediv12a  10527  fiminre  10583  cru  10629  qextltlem  11524  xleadd1a  11568  xmullem  11579  xlemul1a  11603  ixxss12  11684  ioodisj  11791  fsuppmapnn0fz  12240  seqf1o  12286  mulexpz  12344  leexp1a  12363  faclbnd  12507  swrdswrdlem  12852  abs3lem  13450  cau3lem  13466  rlim3  13611  ello12  13629  lo1bdd2  13637  elo12  13640  rlimconst  13657  isercoll  13780  climcau  13783  climbdd  13784  summolem2  13831  fsumconst  13900  o1fsum  13922  incexclem  13943  fprodconst  14081  bitsfzo  14458  dvdsmulgcd  14571  pc2dvds  14877  pcz  14879  pcadd  14883  pcfac  14893  vdwmc2  14978  vdwlem2  14981  vdwlem10  14989  vdw  14993  ramcl  15036  sbcie3s  15216  firest  15380  prdsval  15402  mreexd  15597  mreexexlemd  15599  iscat  15627  cidfval  15631  iscatd2  15636  catcocl  15640  catass  15641  catpropd  15663  cidpropd  15664  moni  15690  monpropd  15691  issubc  15789  subccocl  15799  funcco  15825  funcpropd  15854  fullpropd  15874  nati  15909  natpropd  15930  fucpropd  15931  xpcpropd  16142  curfuncf  16172  curf2ndf  16181  yonffthlem  16216  acsfiindd  16472  mndpropd  16611  mhmeql  16660  isgrpinv  16765  mhmmnd  16857  conjnmzb  16966  gass  17004  symgextf  17107  dfod2  17264  gexdvds  17284  sylow3lem2  17329  efgredlem  17446  efgredeu  17451  ghmcmn  17521  oddvdssubg  17542  dprdfcntz  17697  pgpfaclem3  17765  issrg  17790  isring  17833  dvdsrmul1  17930  issubdrg  18082  islmhm2  18310  lmhmeql  18327  lssacsex  18416  issubassa2  18618  opsrval  18747  isphl  19244  uvcf1  19399  lindfmm  19434  scmatmats  19585  smatvscl  19598  mdetunilem7  19692  gsummatr01lem4  19732  m2cpmfo  19829  decpmatmulsumfsupp  19846  pmatcollpw3fi1lem1  19859  pm2mpf1lem  19867  pm2mpf1  19872  mp2pm2mplem4  19882  pm2mpghm  19889  pm2mpmhmlem1  19891  pm2mpmhmlem2  19892  chfacfscmulfsupp  19932  chfacfpmmulfsupp  19936  cctop  20070  neiptoptop  20196  neiptopreu  20198  tgrest  20224  ordtrest2lem  20268  cnss1  20341  cncnp  20345  isnrm3  20424  uncmp  20467  cmpfi  20472  iuncon  20492  1stcrest  20517  subislly  20545  islly2  20548  cldllycmp  20559  lly1stc  20560  llycmpkgen2  20614  kgencn  20620  xkoccn  20683  ptcnplem  20685  pthaus  20702  txhaus  20711  txkgen  20716  xkohaus  20717  xkococnlem  20723  txcon  20753  regr1lem2  20804  kqreglem1  20805  reghmph  20857  nrmhmph  20858  trfil2  20951  ufileu  20983  flimopn  21039  flimcf  21046  fclscf  21089  ufilcmp  21096  cnpfcf  21105  cnextfun  21128  tgpmulg  21157  symgtgp  21165  tgpt0  21182  qustgplem  21184  ustex2sym  21280  ustex3sym  21281  trust  21293  restutop  21301  restutopopn  21302  ustuqtop2  21306  ustuqtop4  21308  utop3cls  21315  utopreg  21316  cstucnd  21348  ucncn  21349  trcfilu  21358  neipcfilu  21360  ismet2  21397  metequiv2  21574  metcnp  21605  metcnp2  21606  metcnpi3  21610  txmetcnp  21611  metustto  21617  metustsym  21619  metust  21622  cfilucfil  21623  metuel2  21629  psmetutop  21631  restmetu  21634  metucn  21635  ngptgp  21693  tngngp  21711  nmoleub  21785  nmoleubOLD  21801  icccmp  21892  reconnlem2  21894  reconn  21895  xmetdcn2  21904  metdseq0  21920  metdscn  21922  metdseq0OLD  21935  metdscnOLD  21937  elcncf2  21971  cncfmet  21989  cnheibor  22032  nmoleub2lem2  22179  nmoleub3  22182  iscfil2  22285  iscfil3  22292  cfilfcls  22293  equivcfil  22318  caubl  22326  bcthlem5  22345  pmltpc  22450  ovollb2  22491  ovoliunnul  22509  ovolicc2lem4OLD  22522  ovolicc2lem4  22523  volsup  22558  ioorf  22574  ioorfOLD  22579  dyadss  22601  dyaddisjlem  22602  mbfposr  22657  cncombf  22663  mbflimsup  22672  mbflimsupOLD  22673  i1fmulclem  22709  mbfi1fseqlem4  22725  iblss2  22812  ellimc2  22881  ellimc3  22883  dvnadd  22932  dvmptfsum  22976  dvferm1  22986  dvferm2  22988  fta1g  23167  plyeq0lem  23213  plydivex  23299  fta1  23310  aalioulem2  23338  aalioulem3  23339  ulmuni  23396  ulmbdd  23402  ulmdvlem3  23406  mtest  23408  abelthlem8  23443  pilem3  23458  pilem3OLD  23459  efopn  23652  cxpmul2z  23685  cxpcn3lem  23736  jensen  23963  lgambdd  24011  lgamucov  24012  isppw2  24091  sqf11  24115  mersenne  24204  dchrelbas3  24215  dchrptlem1  24241  dchrpt  24244  lgsval2lem  24283  lgsdchrval  24324  lgsquad3  24338  2sqb  24355  pntrsumbnd2  24454  pntpbnd  24475  pntibnd  24480  istrkgc  24551  istrkgb  24552  tglowdim1i  24594  tgbtwndiff  24599  tgifscgr  24602  iscgrglt  24608  tgcgrxfr  24612  lnext  24661  tgbtwnconn1lem3  24668  tgbtwnconn1  24669  legval  24678  legov  24679  legov2  24680  legtrd  24683  legtri3  24684  legso  24693  hlcgrex  24710  hlcgreu  24712  tglnne  24722  tglndim0  24723  tglineeltr  24725  tglinethru  24730  tglnne0  24734  tglnpt2  24735  colline  24743  tglowdim2l  24744  tglowdim2ln  24745  mirreu3  24748  miriso  24764  midexlem  24786  isperp  24806  perpcom  24807  perpneq  24808  isperp2  24809  footex  24812  colperpexlem3  24823  opphllem  24826  midex  24828  oppne3  24834  opptgdim2  24836  opphllem2  24839  opphllem3  24840  opphllem5  24842  opphllem6  24843  opphl  24845  outpasch  24846  lnopp2hpgb  24854  colopp  24860  lmieu  24875  trgcopy  24895  trgcopyeu  24897  iscgra1  24901  cgrane1  24903  cgrane2  24904  cgrane3  24905  cgrahl1  24907  cgrahl2  24908  cgracgr  24909  cgraswap  24911  cgracom  24913  cgratr  24914  cgrabtwn  24916  cgrahl  24917  dfcgra2  24920  sacgr  24921  acopyeu  24924  inaghl  24930  cgrg3col4  24933  f1otrg  24950  f1otrge  24951  axsegcon  25006  axeuclidlem  25041  axcontlem2  25044  usgra1  25149  usgrares1  25187  nbgraf1olem5  25222  pthdepisspth  25353  clwwlkf1  25573  clwwlknscsh  25596  el2spthonot  25647  usg2wotspth  25661  iseupa  25742  eupath2  25757  frgrancvvdeqlem9  25818  friendshipgt3  25898  isgrp2d  26012  smcnlem  26382  0lno  26480  ubthlem1  26561  ubthlem3  26563  chocunii  27003  occl  27006  5oalem1  27356  3oalem2  27365  nmopub2tALT  27611  nmfnleub2  27628  lnconi  27735  kbass5  27822  mdslmd1lem1  28027  mdslmd1lem2  28028  cdj1i  28135  disjabrex  28241  disjabrexf  28242  acunirnmpt  28310  acunirnmpt2  28311  acunirnmpt2f  28312  aciunf1lem  28313  fgreu  28323  xrge0infss  28389  xrge0infssOLD  28390  xrofsup  28402  2sqmo  28459  ressprs  28465  xrge0addgt0  28503  submarchi  28552  isarchi3  28553  archiabllem1  28559  archiabllem2a  28560  gsumle  28591  suborng  28627  isarchiofld  28629  psgnfzto1stlem  28662  fzto1st1  28664  mdetpmtr1  28698  fimaproj  28709  txomap  28710  qtophaus  28712  cmpcref  28726  pstmxmet  28749  sqsscirc1  28763  ordtrest2NEWlem  28777  ordtconlem1  28779  pnfneige0  28806  lmxrge0  28807  lmdvg  28808  qqhval2  28835  esumcst  28933  esumrnmpt2  28938  esumfsup  28940  esumcvg  28956  esum2d  28963  esumiun  28964  sigaclfu2  28992  insiga  29008  ldsysgenld  29031  ldgenpisyslem1  29034  fiunelros  29045  measinb  29092  imambfm  29133  oms0  29174  omssubadd  29177  oms0OLD  29178  omssubaddOLD  29181  carsgclctunlem3  29201  eulerpartlemgvv  29258  dstrvprob  29353  sgnsub  29464  signstfvneq0  29510  afsval  29537  derangenlem  29943  sconpi1  30011  cvmsss2  30046  cvmopnlem  30050  cvmlift3lem7  30097  msrval  30225  ifscgr  30860  cgrxfr  30871  btwnconn1lem13  30915  outsideofeu  30947  neibastop2lem  31065  poimirlem14  31999  poimirlem22  32007  poimirlem29  32014  broucube  32019  heicant  32020  mblfinlem1  32022  itg2addnclem  32038  ftc1cnnc  32061  ftc1anclem7  32068  sstotbnd2  32151  equivtotbnd  32155  isbnd3  32161  ssbnd  32165  totbndbnd  32166  cntotbnd  32173  heibor1lem  32186  rrncmslem  32209  lssats  32623  lsat0cv  32644  lkrlss  32706  lfl1dim  32732  lfl1dim2N  32733  lkrpssN  32774  hlhgt2  32999  3dim2  33078  2dim  33080  lplncvrlvol  33226  paddasslem11  33440  pmapjat1  33463  2polssN  33525  pclfinclN  33560  pexmidlem8N  33587  lhpexle1lem  33617  4atex  33686  ltrnid  33745  trlator0  33782  cdlemg2cex  34203  tendodi1  34396  tendodi2  34397  diblss  34783  dihopelvalcpre  34861  dihatexv  34951  mapdval4N  35245  mzpindd  35633  mzpsubst  35635  mzpcompact2lem  35638  eldioph2b  35650  irrapxlem3  35713  irrapxlem5  35715  pellex  35724  pell1234qrdich  35752  pell14qrexpcl  35758  congabseq  35869  jm2.26a  35900  jm2.26lem3  35901  rmydioph  35914  lnrfg  36023  hbt  36034  4an4132  36899  iunconlem2  37372  fnchoice  37390  cncmpmax  37393  disjf1  37495  supxrge  37599  suplesup  37600  climrec  37719  climsuse  37725  islptre  37737  addlimc  37767  0ellimcdiv  37768  icccncfext  37803  cncfiooicclem1  37809  fperdvper  37828  ioodvbdlimc1lem2  37842  ioodvbdlimc1lem2OLD  37844  ioodvbdlimc2lem  37846  ioodvbdlimc2lemOLD  37847  dvmptfprodlem  37857  dvmptfprod  37858  dvnprodlem2  37860  stoweidlem7  37905  stoweidlem34  37933  stoweidlem52  37951  stoweidlem60  37959  wallispilem3  37967  fourierdlem34  38042  fourierdlem38  38046  fourierdlem39  38047  fourierdlem48  38056  fourierdlem50  38058  fourierdlem51  38059  fourierdlem73  38081  fourierdlem76  38084  fourierdlem77  38085  fourierdlem80  38088  fourierdlem87  38095  fourierdlem103  38111  fourierdlem104  38112  etransclem32  38169  etransclem33  38170  sge0f1o  38262  sge0pr  38274  sge0isum  38307  iundjiun  38336  bgoldbtbndlem2  38939  bgoldbtbndlem3  38940  bgoldbtbnd  38942  upgr1eopALT  39253  usgr1eop  39375  pthdepissPth  39767  usgra2pthspth  39938  mgmhmeql  40076  isrng  40149  2zlidl  40207  lindslinindsimp2  40529  snlindsntor  40537  lincresunit2  40544  islindeps2  40549
  Copyright terms: Public domain W3C validator