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

Theorem simpllr 735
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 447 . 2  |-  ( (
ph  /\  ps )  ->  ps )
21ad2antrr 706 1  |-  ( ( ( ( ph  /\  ps )  /\  ch )  /\  th )  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358
This theorem is referenced by:  simp-4r  743  soisoi  5825  tz7.49  6457  omabs  6645  undom  6950  omxpenlem  6963  fopwdom  6970  findcard3  7100  frfi  7102  finsschain  7162  marypha1lem  7186  wdomtr  7289  cantnfp1  7383  harcard  7611  numacn  7676  infunsdom1  7839  cofsmo  7895  sornom  7903  ssfin4  7936  isf32lem2  7980  fin1a2lem11  8036  fin1a2lem13  8038  ttukeylem3  8138  ttukeylem5  8140  fpwwe2lem13  8264  pwfseq  8286  gchina  8321  r1limwun  8358  00id  8987  addid1  8992  cnegex  8993  negeu  9042  add20  9286  ltmul12a  9612  lediv12a  9649  cru  9738  qextltlem  10529  xleadd1a  10573  xmullem  10584  xlemul1a  10608  ixxss12  10676  ioodisj  10765  seqf1o  11087  mulexpz  11142  leexp1a  11160  faclbnd  11303  abs3lem  11822  cau3lem  11838  rlim3  11972  ello12  11990  lo1bdd2  11998  elo12  12001  rlimconst  12018  o1of2  12086  isercoll  12141  climcau  12144  summolem2  12189  fsumconst  12252  o1fsum  12271  incexclem  12295  bitsfzo  12626  dvdsmulgcd  12733  isprm5  12791  pc2dvds  12931  pcz  12933  pcadd  12937  pcfac  12947  vdwmc2  13026  vdwlem2  13029  vdwlem10  13037  vdw  13041  ramval  13055  ramcl  13076  firest  13337  prdsval  13355  mreexd  13544  mreexexlemd  13546  iscat  13574  cidfval  13578  iscatd2  13583  catcocl  13587  catass  13588  catpropd  13612  cidpropd  13613  moni  13639  monpropd  13640  issubc  13712  subccocl  13719  funcco  13745  funcpropd  13774  fullpropd  13794  nati  13829  natpropd  13850  fucpropd  13851  xpcpropd  13982  curfuncf  14012  curf2ndf  14021  yonffthlem  14056  acsfiindd  14280  mndpropd  14398  mhmeql  14441  isgrpinv  14532  conjnmzb  14717  gass  14755  gasubg  14756  dfod2  14877  gexdvds  14895  sylow3lem2  14939  efgredlem  15056  efgredeu  15061  oddvdssubg  15147  dprdfcntz  15250  pgpfaclem3  15318  isrng  15345  dvdsrmul1  15435  issubdrg  15570  islmhm2  15795  lmhmeql  15812  lssacsex  15897  issubassa2  16084  opsrval  16216  isphl  16532  cctop  16743  tgrest  16890  ordtrest2lem  16933  iscncl  16998  cncls  17003  cnntr  17004  cnss1  17005  cncnp  17009  isnrm3  17087  uncmp  17130  cmpfi  17135  iuncon  17154  1stcfb  17171  1stcrest  17179  subislly  17207  islly2  17210  cldllycmp  17221  lly1stc  17222  llycmpkgen2  17245  kgencn  17251  xkoccn  17313  ptcnplem  17315  pthaus  17332  txhaus  17341  txkgen  17346  xkohaus  17347  xkococnlem  17353  txcon  17383  regr1lem2  17431  kqreglem1  17432  reghmph  17484  nrmhmph  17485  trfil2  17582  ufileu  17614  flimopn  17670  fbflim  17671  flimcf  17677  fclsbas  17716  fclscf  17720  ufilcmp  17727  cnpfcf  17736  tgpmulg  17776  symgtgp  17784  tgpt0  17801  divstgplem  17803  ismet2  17898  metequiv2  18056  metcnp  18087  metcnp2  18088  metcnpi3  18092  txmetcnp  18093  ngptgp  18152  tngngp  18170  nmoi  18237  nmoleub  18240  icccmp  18330  reconnlem2  18332  reconn  18333  xmetdcn2  18342  metdseq0  18358  metdscn  18360  elcncf2  18394  cncfmet  18412  cnheibor  18453  nmoleub2lem2  18597  nmoleub3  18600  iscfil2  18692  fgcfil  18697  iscfil3  18699  cfilfcls  18700  equivcfil  18725  equivcau  18726  caubl  18733  bcthlem5  18750  pmltpc  18810  ovollb2  18848  ovoliunnul  18866  ovolicc2lem4  18879  volsup  18913  ioorf  18928  dyadss  18949  dyaddisjlem  18950  dyadmax  18953  mbfposr  19007  cncombf  19013  mbflimsup  19021  i1fmulclem  19057  mbfi1fseqlem4  19073  itg2cnlem1  19116  iblss  19159  iblss2  19160  ellimc2  19227  ellimc3  19229  dvnadd  19278  dvmptfsum  19322  dvferm1  19332  dvferm2  19334  fta1g  19553  plyeq0lem  19592  plydivex  19677  fta1  19688  aannenlem1  19708  aalioulem2  19713  aalioulem3  19714  ulmbdd  19775  ulmdvlem3  19779  mtest  19781  abelthlem8  19815  pilem3  19829  efopn  20005  cxpmul2z  20038  cxpcn3lem  20087  jensen  20283  isppw2  20353  sqf11  20377  mersenne  20466  dchrelbas3  20477  dchrptlem1  20503  dchrpt  20506  lgsval2lem  20545  lgsqr  20585  lgsdchrval  20586  lgsquad3  20600  2sqb  20617  pntrsumbnd2  20716  pntpbnd  20737  pntibnd  20742  pntlem3  20758  isgrp2d  20902  smcnlem  21270  0lno  21368  ubthlem1  21449  ubthlem3  21451  chocunii  21880  occl  21883  5oalem1  22233  3oalem2  22242  nmopub2tALT  22489  nmfnleub2  22506  lnconi  22613  kbass5  22700  mdslmd1lem1  22905  mdslmd1lem2  22906  cdj1i  23013  xrofsup  23255  sqsscirc1  23292  xrge0addgt0  23331  disjabrex  23359  disjabrexf  23360  pnfneige0  23374  lmxrge0  23375  lmdvg  23376  esumcst  23436  esumcvg  23454  sigaclfu2  23482  insiga  23498  measinb  23548  imambfm  23567  dstrvprob  23672  derangenlem  23702  sconpi1  23770  cvmsss2  23805  cvmopnlem  23809  cvmlift2lem12  23845  cvmlift3lem7  23856  iseupa  23881  eupath2  23904  axsegcon  24555  axeuclidlem  24590  axcontlem2  24593  ifscgr  24667  cgrxfr  24678  btwnconn1lem13  24722  outsideofeu  24754  mgmlion  25337  muldisc  25481  glmrngo  25482  tcnvec  25690  idmon  25817  pdiveql  26168  neibastop2lem  26309  neibastop2  26310  neibastop3  26311  sstotbnd2  26498  equivtotbnd  26502  isbnd3  26508  ssbnd  26512  totbndbnd  26513  cntotbnd  26520  heibor1lem  26533  rrncmslem  26556  mzpindd  26824  mzpsubst  26826  mzpcompact2lem  26829  eldioph2b  26842  diophren  26896  irrapxlem3  26909  irrapxlem4  26910  irrapxlem5  26911  pellex  26920  pell1234qrdich  26946  pell14qrexpcl  26952  congabseq  27061  jm2.26a  27093  jm2.26lem3  27094  rmydioph  27107  uvcf1  27241  lindfmm  27297  lnrfg  27323  hbt  27334  fnchoice  27700  cncmpmax  27703  climrec  27729  climsuse  27734  stoweidlem7  27756  stoweidlem34  27783  stoweidlem52  27801  stoweidlem60  27809  wallispilem3  27816  usgra1  28119  lssats  29202  lsat0cv  29223  lkrlss  29285  lfl1dim  29311  lfl1dim2N  29312  lkrpssN  29353  hlhgt2  29578  3dim2  29657  2dim  29659  lplncvrlvol  29805  paddasslem11  30019  pmapjat1  30042  2polssN  30104  pclfinclN  30139  pexmidlem8N  30166  lhpexle1lem  30196  lhpmatb  30220  4atex  30265  ltrnid  30324  trlator0  30360  cdlemf2  30751  cdlemg2cex  30780  tendodi1  30973  tendodi2  30974  diaglbN  31245  diaintclN  31248  dibglbN  31356  dibintclN  31357  diblss  31360  dihlsscpre  31424  dihopelvalcpre  31438  dihglblem5aN  31482  dihglblem2aN  31483  dih1dimatlem  31519  dihatexv  31528  lcfl8  31692  mapdval4N  31822
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360
  Copyright terms: Public domain W3C validator