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

Theorem simpllr 760
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  768  soisoi  6209  f1o2ndf1  6893  tz7.49  7112  omabs  7298  omxpenlem  7620  fopwdom  7627  findcard3  7765  frfi  7767  finsschain  7829  marypha1lem  7895  wdomtr  8004  cantnfp1  8103  cantnfp1OLD  8129  harcard  8362  numacn  8433  infunsdom1  8596  cofsmo  8652  sornom  8660  ssfin4  8693  fin1a2lem11  8793  fin1a2lem13  8795  ttukeylem5  8896  fpwwe2lem13  9023  pwfseq  9045  mulcmpblnr  9451  00id  9758  addid1  9763  cnegex  9764  negeu  9815  add20  10071  ltmul12a  10405  lediv12a  10445  cru  10535  qextltlem  11412  xleadd1a  11456  xmullem  11467  xlemul1a  11491  ixxss12  11560  ioodisj  11661  fsuppmapnn0fz  12084  seqf1o  12130  mulexpz  12188  leexp1a  12206  faclbnd  12350  swrdswrdlem  12666  abs3lem  13153  cau3lem  13169  rlim3  13303  ello12  13321  lo1bdd2  13329  elo12  13332  rlimconst  13349  isercoll  13472  climcau  13475  climbdd  13476  summolem2  13520  fsumconst  13587  o1fsum  13609  incexclem  13630  fprodconst  13764  bitsfzo  14067  dvdsmulgcd  14174  pc2dvds  14384  pcz  14386  pcadd  14390  pcfac  14400  vdwmc2  14479  vdwlem2  14482  vdwlem10  14490  vdw  14494  ramcl  14529  sbcie3s  14658  firest  14812  prdsval  14834  mreexd  15021  mreexexlemd  15023  iscat  15051  cidfval  15055  iscatd2  15060  catcocl  15064  catass  15065  catpropd  15086  cidpropd  15087  moni  15113  monpropd  15114  issubc  15186  subccocl  15193  funcco  15219  funcpropd  15248  fullpropd  15268  nati  15303  natpropd  15324  fucpropd  15325  xpcpropd  15456  curfuncf  15486  curf2ndf  15495  yonffthlem  15530  acsfiindd  15786  mndpropd  15925  mhmeql  15974  isgrpinv  16079  mhmmnd  16171  conjnmzb  16280  gass  16318  symgextf  16421  dfod2  16565  gexdvds  16583  sylow3lem2  16627  efgredlem  16744  efgredeu  16749  ghmcmn  16819  oddvdssubg  16840  dprdfcntz  17028  dprdfcntzOLD  17034  pgpfaclem3  17113  issrg  17138  isring  17181  dvdsrmul1  17281  issubdrg  17433  islmhm2  17663  lmhmeql  17680  lssacsex  17769  issubassa2  17973  opsrval  18118  isphl  18641  uvcf1  18801  lindfmm  18840  scmatmats  18991  smatvscl  19004  mdetunilem7  19098  gsummatr01lem4  19138  m2cpmfo  19235  decpmatmulsumfsupp  19252  pmatcollpw3fi1lem1  19265  pm2mpf1lem  19273  pm2mpf1  19278  mp2pm2mplem4  19288  pm2mpghm  19295  pm2mpmhmlem1  19297  pm2mpmhmlem2  19298  chfacfscmulfsupp  19338  chfacfpmmulfsupp  19342  cctop  19485  neiptoptop  19610  neiptopreu  19612  tgrest  19638  ordtrest2lem  19682  cnss1  19755  cncnp  19759  isnrm3  19838  uncmp  19881  cmpfi  19886  iuncon  19907  1stcrest  19932  subislly  19960  islly2  19963  cldllycmp  19974  lly1stc  19975  llycmpkgen2  20029  kgencn  20035  xkoccn  20098  ptcnplem  20100  pthaus  20117  txhaus  20126  txkgen  20131  xkohaus  20132  xkococnlem  20138  txcon  20168  regr1lem2  20219  kqreglem1  20220  reghmph  20272  nrmhmph  20273  trfil2  20366  ufileu  20398  flimopn  20454  flimcf  20461  fclscf  20504  ufilcmp  20511  cnpfcf  20520  cnextfun  20542  tgpmulg  20570  symgtgp  20578  tgpt0  20595  qustgplem  20597  ustex2sym  20697  ustex3sym  20698  trust  20710  restutop  20718  restutopopn  20719  ustuqtop2  20723  ustuqtop4  20725  utop3cls  20732  utopreg  20733  cstucnd  20765  ucncn  20766  trcfilu  20775  neipcfilu  20777  ismet2  20814  metequiv2  20991  metcnp  21022  metcnp2  21023  metcnpi3  21027  txmetcnp  21028  metusttoOLD  21038  metustto  21039  metustsymOLD  21042  metustsym  21043  metustOLD  21048  metust  21049  cfilucfilOLD  21050  cfilucfil  21051  metuel2  21060  metutopOLD  21063  psmetutop  21064  restmetu  21068  metucnOLD  21069  metucn  21070  ngptgp  21128  tngngp  21146  nmoleub  21216  icccmp  21308  reconnlem2  21310  reconn  21311  xmetdcn2  21320  metdseq0  21336  metdscn  21338  elcncf2  21372  cncfmet  21390  cnheibor  21433  nmoleub2lem2  21577  nmoleub3  21580  iscfil2  21683  iscfil3  21690  cfilfcls  21691  equivcfil  21716  caubl  21724  bcthlem5  21745  pmltpc  21840  ovollb2  21878  ovoliunnul  21896  ovolicc2lem4  21909  volsup  21944  ioorf  21960  dyadss  21981  dyaddisjlem  21982  mbfposr  22037  cncombf  22043  mbflimsup  22051  i1fmulclem  22087  mbfi1fseqlem4  22103  iblss2  22190  ellimc2  22259  ellimc3  22261  dvnadd  22310  dvmptfsum  22354  dvferm1  22364  dvferm2  22366  fta1g  22546  plyeq0lem  22585  plydivex  22671  fta1  22682  aalioulem2  22707  aalioulem3  22708  ulmuni  22765  ulmbdd  22771  ulmdvlem3  22775  mtest  22777  abelthlem8  22812  pilem3  22826  efopn  23017  cxpmul2z  23050  cxpcn3lem  23099  jensen  23296  isppw2  23367  sqf11  23391  mersenne  23480  dchrelbas3  23491  dchrptlem1  23517  dchrpt  23520  lgsval2lem  23559  lgsdchrval  23600  lgsquad3  23614  2sqb  23631  pntrsumbnd2  23730  pntpbnd  23751  pntibnd  23756  istrkgc  23829  istrkgb  23830  tglowdim1i  23870  tgbtwndiff  23875  tgifscgr  23878  tgcgrxfr  23887  lnext  23932  tgbtwnconn1lem3  23939  tgbtwnconn1  23940  legval  23949  legov  23950  legov2  23951  legtrd  23954  legtri3  23955  legso  23963  tglnne  23986  tglndim0  23987  tglineeltr  23989  tglinethru  23994  tglnne0  23998  tglnpt2  23999  colline  24008  tglowdim2l  24009  tglowdim2ln  24010  mirreu3  24013  miriso  24028  midexlem  24047  isperp  24067  perpcom  24068  perpneq  24069  isperp2  24070  footex  24073  colperpexlem3  24084  opphllem  24087  midex  24089  opptgdim2  24095  opphllem2  24098  opphllem3  24099  opphllem5  24101  opphllem6  24102  opphl  24103  lnopp2hpgb  24110  lmieu  24128  f1otrg  24152  f1otrge  24153  axsegcon  24208  axeuclidlem  24243  axcontlem2  24246  usgra1  24351  usgrares1  24388  nbgraf1olem5  24423  pthdepisspth  24554  clwwlkf1  24774  clwwlknscsh  24797  el2spthonot  24848  usg2wotspth  24862  iseupa  24943  eupath2  24958  frgrancvvdeqlem9  25019  friendshipgt3  25099  isgrp2d  25215  smcnlem  25585  0lno  25683  ubthlem1  25764  ubthlem3  25766  chocunii  26197  occl  26200  5oalem1  26550  3oalem2  26559  nmopub2tALT  26806  nmfnleub2  26823  lnconi  26930  kbass5  27017  mdslmd1lem1  27222  mdslmd1lem2  27223  cdj1i  27330  disjabrex  27421  disjabrexf  27422  fgreu  27491  xrge0infss  27558  xrofsup  27560  2sqmo  27615  ressprs  27621  xrge0addgt0  27659  submarchi  27708  isarchi3  27709  archiabllem1  27715  archiabllem2a  27716  gsumle  27748  suborng  27783  isarchiofld  27785  fimaproj  27814  txomap  27815  qtophaus  27817  cmpcref  27831  pstmxmet  27854  sqsscirc1  27868  ordtrest2NEWlem  27882  ordtconlem1  27884  pnfneige0  27911  lmxrge0  27912  lmdvg  27913  qqhval2  27941  esumcst  28049  esumfsup  28054  esumcvg  28070  sigaclfu2  28099  insiga  28115  measinb  28170  imambfm  28211  oms0  28244  eulerpartlemgvv  28293  dstrvprob  28388  sgnsub  28461  signstfvneq0  28507  afsval  28529  lgambdd  28557  lgamucov  28558  derangenlem  28593  sconpi1  28662  cvmsss2  28697  cvmopnlem  28701  cvmlift3lem7  28748  msrval  28876  ifscgr  29670  cgrxfr  29681  btwnconn1lem13  29725  outsideofeu  29757  heicant  30025  mblfinlem1  30027  itg2addnclem  30042  ftc1cnnc  30065  ftc1anclem7  30072  neibastop2lem  30154  sstotbnd2  30246  equivtotbnd  30250  isbnd3  30256  ssbnd  30260  totbndbnd  30261  cntotbnd  30268  heibor1lem  30281  rrncmslem  30304  mzpindd  30654  mzpsubst  30657  mzpcompact2lem  30660  eldioph2b  30672  irrapxlem3  30736  irrapxlem5  30738  pellex  30747  pell1234qrdich  30773  pell14qrexpcl  30779  congabseq  30888  jm2.26a  30918  jm2.26lem3  30919  rmydioph  30932  lnrfg  31044  hbt  31055  fnchoice  31358  cncmpmax  31361  climrec  31563  climsuse  31568  islptre  31579  addlimc  31608  0ellimcdiv  31609  icccncfext  31644  cncfiooicclem1  31650  fperdvper  31669  ioodvbdlimc1lem2  31683  ioodvbdlimc2lem  31685  dvmptfprodlem  31695  dvmptfprod  31696  dvnprodlem2  31698  stoweidlem7  31743  stoweidlem34  31770  stoweidlem52  31788  stoweidlem60  31796  wallispilem3  31803  fourierdlem34  31877  fourierdlem38  31881  fourierdlem39  31882  fourierdlem48  31891  fourierdlem50  31893  fourierdlem51  31894  fourierdlem73  31916  fourierdlem76  31919  fourierdlem77  31920  fourierdlem80  31923  fourierdlem87  31930  fourierdlem103  31946  fourierdlem104  31947  etransclem32  32003  etransclem33  32004  usgra2pthspth  32305  mgmhmeql  32445  isrng  32520  2zlidl  32567  lindslinindsimp2  32934  snlindsntor  32942  lincresunit2  32949  islindeps2  32954  4an4132  33136  iunconlem2  33603  lssats  34612  lsat0cv  34633  lkrlss  34695  lfl1dim  34721  lfl1dim2N  34722  lkrpssN  34763  hlhgt2  34988  3dim2  35067  2dim  35069  lplncvrlvol  35215  paddasslem11  35429  pmapjat1  35452  2polssN  35514  pclfinclN  35549  pexmidlem8N  35576  lhpexle1lem  35606  4atex  35675  ltrnid  35734  trlator0  35771  cdlemg2cex  36192  tendodi1  36385  tendodi2  36386  diblss  36772  dihopelvalcpre  36850  dihatexv  36940  mapdval4N  37234
  Copyright terms: Public domain W3C validator