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

Theorem simplll 757
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 457 . 2  |-  ( (
ph  /\  ps )  ->  ph )
21ad2antrr 725 1  |-  ( ( ( ( ph  /\  ps )  /\  ch )  /\  th )  ->  ph )
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-4l  765  f1imass  5972  tfrlem1  6827  oeeui  7033  oaabs2  7076  boxcutc  7298  omxpenlem  7404  cantnfle  7871  cantnfleOLD  7901  acndom2  8216  infpwfien  8224  sornom  8438  isf32lem2  8515  isf32lem4  8517  fin1a2lem11  8571  ttukeylem5  8674  pwfseq  8823  gchina  8858  inttsk  8933  inar1  8934  prlem936  9208  00id  9536  mul02lem1  9537  addid1  9541  cnegex  9542  negeu  9592  add20  9843  ltmul12a  10177  lediv12a  10217  cru  10306  qextltlem  11164  xmullem  11219  xlemul1a  11243  ixxss12  11312  ioodisj  11407  elfz0fzfz0  11477  seqf1o  11839  mulexpz  11896  leexp1a  11914  seqcoll  12208  swrdswrdlem  12345  abs3lem  12818  cau3lem  12834  climcau  13140  sumeq2ii  13162  summolem2  13185  climcndslem1  13304  climcndslem2  13305  geomulcvg  13328  mertenslem1  13336  mertenslem2  13337  mertens  13338  bitsfzo  13623  sadadd2lem2  13638  dvdsmulgcd  13730  qredeu  13785  pc2dvds  13937  pcz  13939  ramcl  14082  firest  14363  mreexexlemd  14574  isacs2  14583  iscatd2  14611  ipodrsima  15327  mrelatlub  15348  mndpropd  15438  mhmeql  15483  isgrpinv  15579  mulgnn0dir  15641  issubg4  15691  gasubg  15811  symgextf  15913  pmtr3ncom  15972  gexdvds  16074  oddvdssubg  16328  cyggeninv  16351  cyggenod  16352  issrg  16599  dvdsrmul1  16735  unitgrp  16749  cntzsubr  16877  islmhm2  17099  lmhmeql  17116  lbspropd  17160  lssacsex  17205  issubassa2  17395  mplbas2  17531  mplbas2OLD  17532  psgndiflemA  18011  isphl  18037  ocvocv  18076  lindfmm  18236  mdet1  18388  neissex  18711  neiptoptop  18715  neiptopnei  18716  restbas  18742  tgrest  18743  restopnb  18759  cnpco  18851  isnrm3  18943  isreg2  18961  iuncon  19012  1stcrest  19037  2ndcctbss  19039  2ndcomap  19042  2ndcsep  19043  dislly  19081  kgencn2  19110  ptbasfi  19134  txhaus  19200  txkgen  19205  txcon  19242  qtopcn  19267  regr1lem2  19293  kqnrmlem1  19296  kqnrmlem2  19297  trfbas2  19396  trfil2  19440  flimcf  19535  hauspwpwf1  19540  fclscf  19578  flimfnfcls  19581  cnextcn  19619  ustexsym  19770  ustex2sym  19771  ustex3sym  19772  ustuqtop4  19799  utop3cls  19806  utopreg  19807  ucnima  19836  ucncn  19840  fmucnd  19847  metequiv2  20065  prdsxmslem2  20084  metcnpi3  20101  metusttoOLD  20112  metustto  20113  metustidOLD  20114  metustid  20115  metustexhalfOLD  20118  metustexhalf  20119  ngptgp  20202  xrsblre  20368  icccmp  20382  reconnlem1  20383  reconn  20385  opnreen  20388  metdsf  20404  metdscn  20412  fsumcn  20426  elcncf2  20446  cncfmet  20464  pcoass  20576  lmcau  20803  rrxdstprj1  20888  pmltpc  20914  ivthlem2  20916  ivthlem3  20917  ovollb2  20952  volsup  21017  ioombl1  21023  ioorf  21033  dyadss  21054  dyaddisjlem  21055  dyadmax  21058  volcn  21066  cncombf  21116  mbflimsup  21124  itg2const2  21199  iblss2  21263  cpnord  21389  dvmptfsum  21427  fta1g  21619  plydivex  21743  fta1  21754  aannenlem1  21774  ulmdvlem3  21847  abelthlem8  21884  pilem3  21898  advlogexp  22080  cxpmul2z  22116  atantayl2  22313  jensen  22362  isppw2  22433  lgsqr  22665  lgsdchrval  22666  lgsquad3  22680  2sqb  22697  dchrisumlem3  22720  rpvmasum2  22741  mulog2sumlem2  22764  pntrsumbnd2  22796  f1otrg  23085  f1otrge  23086  axsegcon  23141  axeuclidlem  23176  axcontlem9  23186  eengtrkg  23199  nbgraf1olem5  23322  cusgrasize2inds  23353  0wlkon  23414  0trlon  23415  0pthon  23446  3v3e3cycl2  23518  iseupa  23554  vacn  24057  smcnlem  24060  0lno  24158  chocunii  24672  occl  24675  5oalem1  25025  3oalem2  25034  unoplin  25292  hmoplin  25314  lnconi  25405  kbass5  25492  mdslmd1lem1  25697  mdslmd1lem2  25698  mdsymlem2  25776  cdj1i  25805  disjabrex  25894  disjabrexf  25895  fgreu  25958  xrge0infss  26021  xrofsup  26023  xrge0addgt0  26122  submomnd  26141  submarchi  26171  archiabllem1  26178  archiabllem2a  26179  isarchiofld  26253  rge0scvg  26348  lmxrge0  26351  lmdvg  26352  qqhval2  26380  esumfsup  26488  esumpcvgval  26496  esumcvg  26504  sigaclfu2  26533  sigainb  26548  insiga  26549  measinblem  26603  measinb  26604  measdivcstOLD  26607  measdivcst  26608  oddpwdc  26706  dstrvprob  26823  sgnmul  26894  sgnsub  26896  signsply0  26921  signstfvneq0  26942  ptpcon  27091  sconpi1  27097  rescon  27104  cvmliftmolem2  27140  cvmlift2lem12  27172  prodeq2ii  27395  prodmolem2  27417  poseq  27683  ifscgr  28044  cgrxfr  28055  outsideofeu  28131  linethru  28153  fin2so  28387  mblfinlem2  28400  mblfinlem3  28401  itg2addnclem  28414  ftc1anclem7  28444  ftc1anclem8  28445  ftc1anc  28446  neibastop1  28551  ssbnd  28658  totbndbnd  28659  prtlem10  28981  mzpsubst  29056  mzpcompact2lem  29059  eldioph2  29071  eldioph2b  29072  diophren  29123  pell14qrexpcl  29179  elpell1qr2  29184  monotoddzzfi  29254  acongtr  29292  acongrep  29294  jm2.19lem4  29312  jm2.26a  29320  jm2.26lem3  29321  jm2.26  29322  isnumbasgrplem2  29431  mendassa  29522  stoweidlem7  29773  stoweidlem28  29794  stoweidlem34  29800  stoweidlem48  29814  stoweidlem49  29815  stoweidlem52  29818  stoweidlem57  29823  wallispilem3  29833  ralxfrd2  30108  wlkiswwlk1  30295  usg2wotspth  30374  vdiscusgra  30508  vdn1frgrav2  30589  vdgn1frgrav2  30590  frgrancvvdeqlem9  30605  frgrawopreg  30613  frghash2spot  30627  numclwlk1lem2foa  30655  numclwlk1lem2fo  30659  frgrareggt1  30680  fsuppmapnn0fz  30766  mdetdiag  30867  4animp1  31130  4an4132  31132  bnj1408  31956  lssats  32550  lkrlss  32633  lshpset2N  32657  2dim  33007  islvol5  33116  paddasslem11  33367  pexmidlem8N  33514  ltrnid  33672  idltrn  33687  trlator0  33708  trlnidatb  33714  cdlemf2  34099  cdlemg2cex  34128  tendodi1  34321  tendodi2  34322  diblss  34708  dihopelvalcpre  34786  dih1dimatlem  34867  dihglblem6  34878
  Copyright terms: Public domain W3C validator