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 459 . 2  |-  ( (
ph  /\  ps )  ->  ps )
21ad2antrr 723 1  |-  ( ( ( ( ph  /\  ps )  /\  ch )  /\  th )  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367
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 369
This theorem is referenced by:  simp-4r  766  soisoi  6125  f1o2ndf1  6807  tz7.49  7028  omabs  7214  omxpenlem  7537  fopwdom  7544  findcard3  7678  frfi  7680  finsschain  7742  marypha1lem  7808  wdomtr  7916  cantnfp1  8013  cantnfp1OLD  8039  harcard  8272  numacn  8343  infunsdom1  8506  cofsmo  8562  sornom  8570  ssfin4  8603  fin1a2lem11  8703  fin1a2lem13  8705  ttukeylem5  8806  fpwwe2lem13  8931  pwfseq  8953  mulcmpblnr  9359  00id  9666  addid1  9671  cnegex  9672  negeu  9723  add20  9982  ltmul12a  10315  lediv12a  10354  cru  10444  qextltlem  11322  xleadd1a  11366  xmullem  11377  xlemul1a  11401  ixxss12  11470  ioodisj  11571  fsuppmapnn0fz  12005  seqf1o  12051  mulexpz  12109  leexp1a  12127  faclbnd  12270  swrdswrdlem  12595  abs3lem  13173  cau3lem  13189  rlim3  13323  ello12  13341  lo1bdd2  13349  elo12  13352  rlimconst  13369  isercoll  13492  climcau  13495  climbdd  13496  summolem2  13540  fsumconst  13607  o1fsum  13629  incexclem  13650  fprodconst  13784  bitsfzo  14087  dvdsmulgcd  14194  pc2dvds  14404  pcz  14406  pcadd  14410  pcfac  14420  vdwmc2  14499  vdwlem2  14502  vdwlem10  14510  vdw  14514  ramcl  14549  sbcie3s  14680  firest  14840  prdsval  14862  mreexd  15049  mreexexlemd  15051  iscat  15079  cidfval  15083  iscatd2  15088  catcocl  15092  catass  15093  catpropd  15115  cidpropd  15116  moni  15142  monpropd  15143  issubc  15241  subccocl  15251  funcco  15277  funcpropd  15306  fullpropd  15326  nati  15361  natpropd  15382  fucpropd  15383  xpcpropd  15594  curfuncf  15624  curf2ndf  15633  yonffthlem  15668  acsfiindd  15924  mndpropd  16063  mhmeql  16112  isgrpinv  16217  mhmmnd  16309  conjnmzb  16418  gass  16456  symgextf  16559  dfod2  16703  gexdvds  16721  sylow3lem2  16765  efgredlem  16882  efgredeu  16887  ghmcmn  16957  oddvdssubg  16978  dprdfcntz  17162  dprdfcntzOLD  17168  pgpfaclem3  17247  issrg  17272  isring  17315  dvdsrmul1  17415  issubdrg  17567  islmhm2  17797  lmhmeql  17814  lssacsex  17903  issubassa2  18107  opsrval  18252  isphl  18754  uvcf1  18912  lindfmm  18947  scmatmats  19098  smatvscl  19111  mdetunilem7  19205  gsummatr01lem4  19245  m2cpmfo  19342  decpmatmulsumfsupp  19359  pmatcollpw3fi1lem1  19372  pm2mpf1lem  19380  pm2mpf1  19385  mp2pm2mplem4  19395  pm2mpghm  19402  pm2mpmhmlem1  19404  pm2mpmhmlem2  19405  chfacfscmulfsupp  19445  chfacfpmmulfsupp  19449  cctop  19592  neiptoptop  19718  neiptopreu  19720  tgrest  19746  ordtrest2lem  19790  cnss1  19863  cncnp  19867  isnrm3  19946  uncmp  19989  cmpfi  19994  iuncon  20014  1stcrest  20039  subislly  20067  islly2  20070  cldllycmp  20081  lly1stc  20082  llycmpkgen2  20136  kgencn  20142  xkoccn  20205  ptcnplem  20207  pthaus  20224  txhaus  20233  txkgen  20238  xkohaus  20239  xkococnlem  20245  txcon  20275  regr1lem2  20326  kqreglem1  20327  reghmph  20379  nrmhmph  20380  trfil2  20473  ufileu  20505  flimopn  20561  flimcf  20568  fclscf  20611  ufilcmp  20618  cnpfcf  20627  cnextfun  20649  tgpmulg  20677  symgtgp  20685  tgpt0  20702  qustgplem  20704  ustex2sym  20804  ustex3sym  20805  trust  20817  restutop  20825  restutopopn  20826  ustuqtop2  20830  ustuqtop4  20832  utop3cls  20839  utopreg  20840  cstucnd  20872  ucncn  20873  trcfilu  20882  neipcfilu  20884  ismet2  20921  metequiv2  21098  metcnp  21129  metcnp2  21130  metcnpi3  21134  txmetcnp  21135  metusttoOLD  21145  metustto  21146  metustsymOLD  21149  metustsym  21150  metustOLD  21155  metust  21156  cfilucfilOLD  21157  cfilucfil  21158  metuel2  21167  metutopOLD  21170  psmetutop  21171  restmetu  21175  metucnOLD  21176  metucn  21177  ngptgp  21235  tngngp  21253  nmoleub  21323  icccmp  21415  reconnlem2  21417  reconn  21418  xmetdcn2  21427  metdseq0  21443  metdscn  21445  elcncf2  21479  cncfmet  21497  cnheibor  21540  nmoleub2lem2  21684  nmoleub3  21687  iscfil2  21790  iscfil3  21797  cfilfcls  21798  equivcfil  21823  caubl  21831  bcthlem5  21852  pmltpc  21947  ovollb2  21985  ovoliunnul  22003  ovolicc2lem4  22016  volsup  22051  ioorf  22067  dyadss  22088  dyaddisjlem  22089  mbfposr  22144  cncombf  22150  mbflimsup  22158  i1fmulclem  22194  mbfi1fseqlem4  22210  iblss2  22297  ellimc2  22366  ellimc3  22368  dvnadd  22417  dvmptfsum  22461  dvferm1  22471  dvferm2  22473  fta1g  22653  plyeq0lem  22692  plydivex  22778  fta1  22789  aalioulem2  22814  aalioulem3  22815  ulmuni  22872  ulmbdd  22878  ulmdvlem3  22882  mtest  22884  abelthlem8  22919  pilem3  22933  efopn  23126  cxpmul2z  23159  cxpcn3lem  23208  jensen  23435  isppw2  23506  sqf11  23530  mersenne  23619  dchrelbas3  23630  dchrptlem1  23656  dchrpt  23659  lgsval2lem  23698  lgsdchrval  23739  lgsquad3  23753  2sqb  23770  pntrsumbnd2  23869  pntpbnd  23890  pntibnd  23895  istrkgc  23968  istrkgb  23969  tglowdim1i  24012  tgbtwndiff  24017  tgifscgr  24020  tgcgrxfr  24029  lnext  24074  tgbtwnconn1lem3  24081  tgbtwnconn1  24082  legval  24091  legov  24092  legov2  24093  legtrd  24096  legtri3  24097  legso  24105  tglnne  24128  tglndim0  24129  tglineeltr  24131  tglinethru  24136  tglnne0  24140  tglnpt2  24141  colline  24150  tglowdim2l  24151  tglowdim2ln  24152  mirreu3  24155  miriso  24170  midexlem  24189  isperp  24209  perpcom  24210  perpneq  24211  isperp2  24212  footex  24215  colperpexlem3  24226  opphllem  24229  midex  24231  opptgdim2  24237  opphllem2  24240  opphllem3  24241  opphllem5  24243  opphllem6  24244  opphl  24245  lnopp2hpgb  24252  lmieu  24270  f1otrg  24295  f1otrge  24296  axsegcon  24351  axeuclidlem  24386  axcontlem2  24389  usgra1  24494  usgrares1  24531  nbgraf1olem5  24566  pthdepisspth  24697  clwwlkf1  24917  clwwlknscsh  24940  el2spthonot  24991  usg2wotspth  25005  iseupa  25086  eupath2  25101  frgrancvvdeqlem9  25162  friendshipgt3  25242  isgrp2d  25354  smcnlem  25724  0lno  25822  ubthlem1  25903  ubthlem3  25905  chocunii  26336  occl  26339  5oalem1  26689  3oalem2  26698  nmopub2tALT  26944  nmfnleub2  26961  lnconi  27068  kbass5  27155  mdslmd1lem1  27360  mdslmd1lem2  27361  cdj1i  27468  disjabrex  27572  disjabrexf  27573  acunirnmpt  27645  acunirnmpt2  27646  acunirnmpt2f  27647  aciunf1lem  27648  fgreu  27659  xrge0infss  27730  xrofsup  27735  2sqmo  27790  ressprs  27796  xrge0addgt0  27834  submarchi  27883  isarchi3  27884  archiabllem1  27890  archiabllem2a  27891  gsumle  27923  suborng  27959  isarchiofld  27961  fimaproj  27990  txomap  27991  qtophaus  27993  cmpcref  28007  pstmxmet  28030  sqsscirc1  28044  ordtrest2NEWlem  28058  ordtconlem1  28060  pnfneige0  28087  lmxrge0  28088  lmdvg  28089  qqhval2  28116  esumcst  28211  esumrnmpt2  28216  esumfsup  28218  esumcvg  28234  esum2d  28241  esumiun  28242  sigaclfu2  28270  insiga  28286  measinb  28348  imambfm  28389  oms0  28424  omssubadd  28427  carsgclctunlem3  28447  eulerpartlemgvv  28498  dstrvprob  28593  sgnsub  28666  signstfvneq0  28712  afsval  28734  lgambdd  28768  lgamucov  28769  derangenlem  28804  sconpi1  28873  cvmsss2  28908  cvmopnlem  28912  cvmlift3lem7  28959  msrval  29087  ifscgr  29847  cgrxfr  29858  btwnconn1lem13  29902  outsideofeu  29934  heicant  30214  mblfinlem1  30216  itg2addnclem  30232  ftc1cnnc  30255  ftc1anclem7  30262  neibastop2lem  30344  sstotbnd2  30436  equivtotbnd  30440  isbnd3  30446  ssbnd  30450  totbndbnd  30451  cntotbnd  30458  heibor1lem  30471  rrncmslem  30494  mzpindd  30844  mzpsubst  30846  mzpcompact2lem  30849  eldioph2b  30861  irrapxlem3  30925  irrapxlem5  30927  pellex  30936  pell1234qrdich  30962  pell14qrexpcl  30968  congabseq  31077  jm2.26a  31108  jm2.26lem3  31109  rmydioph  31122  lnrfg  31236  hbt  31247  fnchoice  31571  cncmpmax  31574  climrec  31775  climsuse  31780  islptre  31791  addlimc  31820  0ellimcdiv  31821  icccncfext  31856  cncfiooicclem1  31862  fperdvper  31881  ioodvbdlimc1lem2  31895  ioodvbdlimc2lem  31897  dvmptfprodlem  31907  dvmptfprod  31908  dvnprodlem2  31910  stoweidlem7  31955  stoweidlem34  31982  stoweidlem52  32000  stoweidlem60  32008  wallispilem3  32015  fourierdlem34  32089  fourierdlem38  32093  fourierdlem39  32094  fourierdlem48  32103  fourierdlem50  32105  fourierdlem51  32106  fourierdlem73  32128  fourierdlem76  32131  fourierdlem77  32132  fourierdlem80  32135  fourierdlem87  32142  fourierdlem103  32158  fourierdlem104  32159  etransclem32  32215  etransclem33  32216  usgra2pthspth  32669  mgmhmeql  32809  isrng  32882  2zlidl  32940  lindslinindsimp2  33264  snlindsntor  33272  lincresunit2  33279  islindeps2  33284  4an4132  33601  iunconlem2  34082  lssats  35150  lsat0cv  35171  lkrlss  35233  lfl1dim  35259  lfl1dim2N  35260  lkrpssN  35301  hlhgt2  35526  3dim2  35605  2dim  35607  lplncvrlvol  35753  paddasslem11  35967  pmapjat1  35990  2polssN  36052  pclfinclN  36087  pexmidlem8N  36114  lhpexle1lem  36144  4atex  36213  ltrnid  36272  trlator0  36309  cdlemg2cex  36730  tendodi1  36923  tendodi2  36924  diblss  37310  dihopelvalcpre  37388  dihatexv  37478  mapdval4N  37772
  Copyright terms: Public domain W3C validator