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

Theorem simplll 735
Description: Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.)
Assertion
Ref Expression
simplll  |-  ( ( ( ( ph  /\  ps )  /\  ch )  /\  th )  ->  ph )

Proof of Theorem simplll
StepHypRef Expression
1 simpl 444 . 2  |-  ( (
ph  /\  ps )  ->  ph )
21ad2antrr 707 1  |-  ( ( ( ( ph  /\  ps )  /\  ch )  /\  th )  ->  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359
This theorem is referenced by:  simp-4l  743  f1imass  5969  oeeui  6804  oaabs2  6847  boxcutc  7064  omxpenlem  7168  cantnfle  7582  acndom2  7891  infpwfien  7899  sornom  8113  isf32lem2  8190  isf32lem4  8192  fin1a2lem11  8246  ttukeylem5  8349  pwfseq  8495  gchina  8530  inttsk  8605  inar1  8606  prlem936  8880  00id  9197  mul02lem1  9198  addid1  9202  cnegex  9203  negeu  9252  add20  9496  ltmul12a  9822  lediv12a  9859  cru  9948  qextltlem  10744  xmullem  10799  xlemul1a  10823  ixxss12  10892  ioodisj  10982  seqf1o  11319  mulexpz  11375  leexp1a  11393  seqcoll  11667  abs3lem  12097  cau3lem  12113  climcau  12419  sumeq2ii  12442  summolem2  12465  climcndslem1  12584  climcndslem2  12585  geomulcvg  12608  mertenslem1  12616  mertenslem2  12617  mertens  12618  bitsfzo  12902  sadadd2lem2  12917  dvdsmulgcd  13009  qredeu  13062  pc2dvds  13207  pcz  13209  ramcl  13352  firest  13615  mreexexlemd  13824  isacs2  13833  iscatd2  13861  ipodrsima  14546  mrelatlub  14567  mndpropd  14676  mhmeql  14719  isgrpinv  14810  mulgnn0dir  14868  issubg4  14916  gasubg  15034  gexdvds  15173  oddvdssubg  15425  cyggeninv  15448  cyggenod  15449  dvdsrmul1  15713  unitgrp  15727  cntzsubr  15855  islmhm2  16069  lmhmeql  16086  lbspropd  16126  lssacsex  16171  issubassa2  16358  mplbas2  16486  isphl  16814  ocvocv  16853  neissex  17146  neiptoptop  17150  neiptopnei  17151  restbas  17176  tgrest  17177  restopnb  17193  cnpco  17285  isnrm3  17377  isreg2  17395  iuncon  17444  1stcrest  17469  2ndcctbss  17471  2ndcomap  17474  2ndcsep  17475  dislly  17513  kgencn2  17542  ptbasfi  17566  txhaus  17632  txkgen  17637  txcon  17674  qtopcn  17699  regr1lem2  17725  kqnrmlem1  17728  kqnrmlem2  17729  trfbas2  17828  trfil2  17872  flimcf  17967  hauspwpwf1  17972  fclscf  18010  flimfnfcls  18013  cnextcn  18051  ustexsym  18198  ustex2sym  18199  ustex3sym  18200  ustuqtop4  18227  utop3cls  18234  utopreg  18235  ucnima  18264  ucncn  18268  fmucnd  18275  metequiv2  18493  prdsxmslem2  18512  metcnpi3  18529  metusttoOLD  18540  metustto  18541  metustidOLD  18542  metustid  18543  metustexhalfOLD  18546  metustexhalf  18547  ngptgp  18630  xrsblre  18795  icccmp  18809  reconnlem1  18810  reconn  18812  opnreen  18815  metdsf  18831  metdscn  18839  fsumcn  18853  elcncf2  18873  cncfmet  18891  pcoass  19002  lmcau  19218  pmltpc  19300  ivthlem2  19302  ivthlem3  19303  ovollb2  19338  volsup  19403  ioombl1  19409  ioorf  19418  dyadss  19439  dyaddisjlem  19440  dyadmax  19443  volcn  19451  cncombf  19503  mbflimsup  19511  itg2const2  19586  iblss2  19650  cpnord  19774  dvmptfsum  19812  fta1g  20043  plydivex  20167  fta1  20178  aannenlem1  20198  ulmdvlem3  20271  abelthlem8  20308  pilem3  20322  advlogexp  20499  cxpmul2z  20535  atantayl2  20731  jensen  20780  isppw2  20851  lgsqr  21083  lgsdchrval  21084  lgsquad3  21098  2sqb  21115  dchrisumlem3  21138  rpvmasum2  21159  mulog2sumlem2  21182  pntrsumbnd2  21214  nbgraf1olem5  21408  cusgrasize2inds  21439  0wlkon  21500  0trlon  21501  0pthon  21532  3v3e3cycl2  21604  iseupa  21640  vacn  22143  smcnlem  22146  0lno  22244  chocunii  22756  occl  22759  5oalem1  23109  3oalem2  23118  unoplin  23376  hmoplin  23398  lnconi  23489  kbass5  23576  mdslmd1lem1  23781  mdslmd1lem2  23782  mdsymlem2  23860  cdj1i  23889  disjabrex  23977  disjabrexf  23978  xrofsup  24079  xrge0addgt0  24167  rge0scvg  24288  lmxrge0  24290  lmdvg  24291  qqhval2  24319  esumfsup  24413  esumpcvgval  24421  esumcvg  24429  sigaclfu2  24457  sigainb  24472  insiga  24473  measinblem  24527  measinb  24528  measdivcstOLD  24531  measdivcst  24532  dstrvprob  24682  ptpcon  24873  sconpi1  24879  rescon  24886  cvmliftmolem2  24922  cvmlift2lem12  24954  prodeq2ii  25192  prodmolem2  25214  poseq  25467  axsegcon  25770  axeuclidlem  25805  axcontlem9  25815  ifscgr  25882  cgrxfr  25893  outsideofeu  25969  linethru  25991  mblfinlem  26143  mblfinlem2  26144  itg2addnclem  26155  neibastop1  26278  ssbnd  26387  totbndbnd  26388  prtlem10  26604  mzpsubst  26695  mzpcompact2lem  26698  eldioph2  26710  eldioph2b  26711  diophren  26764  pell14qrexpcl  26820  elpell1qr2  26825  monotoddzzfi  26895  acongtr  26933  acongrep  26935  jm2.19lem4  26953  jm2.26a  26961  jm2.26lem3  26962  jm2.26  26963  isnumbasgrplem2  27137  lindfmm  27165  mendassa  27370  stoweidlem7  27623  stoweidlem28  27644  stoweidlem34  27650  stoweidlem48  27664  stoweidlem49  27665  stoweidlem52  27668  stoweidlem57  27673  wallispilem3  27683  swrdswrdlem  28010  usg2wotspth  28081  vdn1frgrav2  28130  vdgn1frgrav2  28131  frgrancvvdeqlem9  28144  frgrawopreg  28152  frghash2spot  28166  bnj1408  29111  lssats  29495  lkrlss  29578  lshpset2N  29602  2dim  29952  islvol5  30061  paddasslem11  30312  pexmidlem8N  30459  ltrnid  30617  idltrn  30632  trlator0  30653  trlnidatb  30659  cdlemf2  31044  cdlemg2cex  31073  tendodi1  31266  tendodi2  31267  diblss  31653  dihopelvalcpre  31731  dih1dimatlem  31812  dihglblem6  31823
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 178  df-an 361
  Copyright terms: Public domain W3C validator