MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  simplll Structured version   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  6010  oeeui  6845  oaabs2  6888  boxcutc  7105  omxpenlem  7209  cantnfle  7626  acndom2  7935  infpwfien  7943  sornom  8157  isf32lem2  8234  isf32lem4  8236  fin1a2lem11  8290  ttukeylem5  8393  pwfseq  8539  gchina  8574  inttsk  8649  inar1  8650  prlem936  8924  00id  9241  mul02lem1  9242  addid1  9246  cnegex  9247  negeu  9296  add20  9540  ltmul12a  9866  lediv12a  9903  cru  9992  qextltlem  10788  xmullem  10843  xlemul1a  10867  ixxss12  10936  ioodisj  11026  seqf1o  11364  mulexpz  11420  leexp1a  11438  seqcoll  11712  abs3lem  12142  cau3lem  12158  climcau  12464  sumeq2ii  12487  summolem2  12510  climcndslem1  12629  climcndslem2  12630  geomulcvg  12653  mertenslem1  12661  mertenslem2  12662  mertens  12663  bitsfzo  12947  sadadd2lem2  12962  dvdsmulgcd  13054  qredeu  13107  pc2dvds  13252  pcz  13254  ramcl  13397  firest  13660  mreexexlemd  13869  isacs2  13878  iscatd2  13906  ipodrsima  14591  mrelatlub  14612  mndpropd  14721  mhmeql  14764  isgrpinv  14855  mulgnn0dir  14913  issubg4  14961  gasubg  15079  gexdvds  15218  oddvdssubg  15470  cyggeninv  15493  cyggenod  15494  dvdsrmul1  15758  unitgrp  15772  cntzsubr  15900  islmhm2  16114  lmhmeql  16131  lbspropd  16171  lssacsex  16216  issubassa2  16403  mplbas2  16531  isphl  16859  ocvocv  16898  neissex  17191  neiptoptop  17195  neiptopnei  17196  restbas  17222  tgrest  17223  restopnb  17239  cnpco  17331  isnrm3  17423  isreg2  17441  iuncon  17491  1stcrest  17516  2ndcctbss  17518  2ndcomap  17521  2ndcsep  17522  dislly  17560  kgencn2  17589  ptbasfi  17613  txhaus  17679  txkgen  17684  txcon  17721  qtopcn  17746  regr1lem2  17772  kqnrmlem1  17775  kqnrmlem2  17776  trfbas2  17875  trfil2  17919  flimcf  18014  hauspwpwf1  18019  fclscf  18057  flimfnfcls  18060  cnextcn  18098  ustexsym  18245  ustex2sym  18246  ustex3sym  18247  ustuqtop4  18274  utop3cls  18281  utopreg  18282  ucnima  18311  ucncn  18315  fmucnd  18322  metequiv2  18540  prdsxmslem2  18559  metcnpi3  18576  metusttoOLD  18587  metustto  18588  metustidOLD  18589  metustid  18590  metustexhalfOLD  18593  metustexhalf  18594  ngptgp  18677  xrsblre  18842  icccmp  18856  reconnlem1  18857  reconn  18859  opnreen  18862  metdsf  18878  metdscn  18886  fsumcn  18900  elcncf2  18920  cncfmet  18938  pcoass  19049  lmcau  19265  pmltpc  19347  ivthlem2  19349  ivthlem3  19350  ovollb2  19385  volsup  19450  ioombl1  19456  ioorf  19465  dyadss  19486  dyaddisjlem  19487  dyadmax  19490  volcn  19498  cncombf  19550  mbflimsup  19558  itg2const2  19633  iblss2  19697  cpnord  19821  dvmptfsum  19859  fta1g  20090  plydivex  20214  fta1  20225  aannenlem1  20245  ulmdvlem3  20318  abelthlem8  20355  pilem3  20369  advlogexp  20546  cxpmul2z  20582  atantayl2  20778  jensen  20827  isppw2  20898  lgsqr  21130  lgsdchrval  21131  lgsquad3  21145  2sqb  21162  dchrisumlem3  21185  rpvmasum2  21206  mulog2sumlem2  21229  pntrsumbnd2  21261  nbgraf1olem5  21455  cusgrasize2inds  21486  0wlkon  21547  0trlon  21548  0pthon  21579  3v3e3cycl2  21651  iseupa  21687  vacn  22190  smcnlem  22193  0lno  22291  chocunii  22803  occl  22806  5oalem1  23156  3oalem2  23165  unoplin  23423  hmoplin  23445  lnconi  23536  kbass5  23623  mdslmd1lem1  23828  mdslmd1lem2  23829  mdsymlem2  23907  cdj1i  23936  disjabrex  24024  disjabrexf  24025  xrofsup  24126  xrge0addgt0  24214  rge0scvg  24335  lmxrge0  24337  lmdvg  24338  qqhval2  24366  esumfsup  24460  esumpcvgval  24468  esumcvg  24476  sigaclfu2  24504  sigainb  24519  insiga  24520  measinblem  24574  measinb  24575  measdivcstOLD  24578  measdivcst  24579  dstrvprob  24729  ptpcon  24920  sconpi1  24926  rescon  24933  cvmliftmolem2  24969  cvmlift2lem12  25001  prodeq2ii  25239  prodmolem2  25261  poseq  25528  axsegcon  25866  axeuclidlem  25901  axcontlem9  25911  ifscgr  25978  cgrxfr  25989  outsideofeu  26065  linethru  26087  mblfinlem2  26244  mblfinlem3  26245  itg2addnclem  26256  ftc1anclem7  26286  ftc1anclem8  26287  ftc1anc  26288  neibastop1  26388  ssbnd  26497  totbndbnd  26498  prtlem10  26714  mzpsubst  26805  mzpcompact2lem  26808  eldioph2  26820  eldioph2b  26821  diophren  26874  pell14qrexpcl  26930  elpell1qr2  26935  monotoddzzfi  27005  acongtr  27043  acongrep  27045  jm2.19lem4  27063  jm2.26a  27071  jm2.26lem3  27072  jm2.26  27073  isnumbasgrplem2  27246  lindfmm  27274  mendassa  27479  stoweidlem7  27732  stoweidlem28  27753  stoweidlem34  27759  stoweidlem48  27773  stoweidlem49  27774  stoweidlem52  27777  stoweidlem57  27782  wallispilem3  27792  ralxfrd2  28072  elfz0fzfz0  28114  swrdswrdlem  28198  2cshw1lem2  28249  usg2wotspth  28351  vdn1frgrav2  28416  vdgn1frgrav2  28417  frgrancvvdeqlem9  28430  frgrawopreg  28438  frghash2spot  28452  4animp1  28580  4an4132  28582  bnj1408  29405  lssats  29810  lkrlss  29893  lshpset2N  29917  2dim  30267  islvol5  30376  paddasslem11  30627  pexmidlem8N  30774  ltrnid  30932  idltrn  30947  trlator0  30968  trlnidatb  30974  cdlemf2  31359  cdlemg2cex  31388  tendodi1  31581  tendodi2  31582  diblss  31968  dihopelvalcpre  32046  dih1dimatlem  32127  dihglblem6  32138
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