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

Theorem simplll 750
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 454 . 2  |-  ( (
ph  /\  ps )  ->  ph )
21ad2antrr 718 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  758  f1imass  5964  tfrlem1  6821  oeeui  7029  oaabs2  7072  boxcutc  7294  omxpenlem  7400  cantnfle  7867  cantnfleOLD  7897  acndom2  8212  infpwfien  8220  sornom  8434  isf32lem2  8511  isf32lem4  8513  fin1a2lem11  8567  ttukeylem5  8670  pwfseq  8819  gchina  8854  inttsk  8929  inar1  8930  prlem936  9204  00id  9532  mul02lem1  9533  addid1  9537  cnegex  9538  negeu  9588  add20  9839  ltmul12a  10173  lediv12a  10213  cru  10302  qextltlem  11160  xmullem  11215  xlemul1a  11239  ixxss12  11308  ioodisj  11402  elfz0fzfz0  11472  seqf1o  11831  mulexpz  11888  leexp1a  11906  seqcoll  12200  swrdswrdlem  12337  abs3lem  12810  cau3lem  12826  climcau  13132  sumeq2ii  13154  summolem2  13177  climcndslem1  13295  climcndslem2  13296  geomulcvg  13319  mertenslem1  13327  mertenslem2  13328  mertens  13329  bitsfzo  13614  sadadd2lem2  13629  dvdsmulgcd  13721  qredeu  13776  pc2dvds  13928  pcz  13930  ramcl  14073  firest  14354  mreexexlemd  14565  isacs2  14574  iscatd2  14602  ipodrsima  15318  mrelatlub  15339  mndpropd  15429  mhmeql  15474  isgrpinv  15568  mulgnn0dir  15630  issubg4  15680  gasubg  15800  symgextf  15902  pmtr3ncom  15961  gexdvds  16063  oddvdssubg  16317  cyggeninv  16340  cyggenod  16341  dvdsrmul1  16679  unitgrp  16693  cntzsubr  16821  islmhm2  17041  lmhmeql  17058  lbspropd  17102  lssacsex  17147  issubassa2  17337  mplbas2  17483  mplbas2OLD  17484  psgndiflemA  17873  isphl  17899  ocvocv  17938  lindfmm  18098  mdet1  18250  neissex  18573  neiptoptop  18577  neiptopnei  18578  restbas  18604  tgrest  18605  restopnb  18621  cnpco  18713  isnrm3  18805  isreg2  18823  iuncon  18874  1stcrest  18899  2ndcctbss  18901  2ndcomap  18904  2ndcsep  18905  dislly  18943  kgencn2  18972  ptbasfi  18996  txhaus  19062  txkgen  19067  txcon  19104  qtopcn  19129  regr1lem2  19155  kqnrmlem1  19158  kqnrmlem2  19159  trfbas2  19258  trfil2  19302  flimcf  19397  hauspwpwf1  19402  fclscf  19440  flimfnfcls  19443  cnextcn  19481  ustexsym  19632  ustex2sym  19633  ustex3sym  19634  ustuqtop4  19661  utop3cls  19668  utopreg  19669  ucnima  19698  ucncn  19702  fmucnd  19709  metequiv2  19927  prdsxmslem2  19946  metcnpi3  19963  metusttoOLD  19974  metustto  19975  metustidOLD  19976  metustid  19977  metustexhalfOLD  19980  metustexhalf  19981  ngptgp  20064  xrsblre  20230  icccmp  20244  reconnlem1  20245  reconn  20247  opnreen  20250  metdsf  20266  metdscn  20274  fsumcn  20288  elcncf2  20308  cncfmet  20326  pcoass  20438  lmcau  20665  rrxdstprj1  20750  pmltpc  20776  ivthlem2  20778  ivthlem3  20779  ovollb2  20814  volsup  20879  ioombl1  20885  ioorf  20895  dyadss  20916  dyaddisjlem  20917  dyadmax  20920  volcn  20928  cncombf  20978  mbflimsup  20986  itg2const2  21061  iblss2  21125  cpnord  21251  dvmptfsum  21289  fta1g  21524  plydivex  21648  fta1  21659  aannenlem1  21679  ulmdvlem3  21752  abelthlem8  21789  pilem3  21803  advlogexp  21985  cxpmul2z  22021  atantayl2  22218  jensen  22267  isppw2  22338  lgsqr  22570  lgsdchrval  22571  lgsquad3  22585  2sqb  22602  dchrisumlem3  22625  rpvmasum2  22646  mulog2sumlem2  22669  pntrsumbnd2  22701  f1otrg  22940  f1otrge  22941  axsegcon  22996  axeuclidlem  23031  axcontlem9  23041  eengtrkg  23054  nbgraf1olem5  23177  cusgrasize2inds  23208  0wlkon  23269  0trlon  23270  0pthon  23301  3v3e3cycl2  23373  iseupa  23409  vacn  23912  smcnlem  23915  0lno  24013  chocunii  24527  occl  24530  5oalem1  24880  3oalem2  24889  unoplin  25147  hmoplin  25169  lnconi  25260  kbass5  25347  mdslmd1lem1  25552  mdslmd1lem2  25553  mdsymlem2  25631  cdj1i  25660  disjabrex  25750  disjabrexf  25751  fgreu  25814  xrofsup  25878  xrge0addgt0  25977  submomnd  25997  submarchi  26027  archiabllem1  26034  archiabllem2a  26035  issrg  26042  isarchiofld  26138  rge0scvg  26233  lmxrge0  26236  lmdvg  26237  qqhval2  26265  esumfsup  26373  esumpcvgval  26381  esumcvg  26389  sigaclfu2  26418  sigainb  26433  insiga  26434  measinblem  26488  measinb  26489  measdivcstOLD  26492  measdivcst  26493  oddpwdc  26585  dstrvprob  26702  sgnmul  26773  sgnsub  26775  signsply0  26800  signstfvneq0  26821  ptpcon  26970  sconpi1  26976  rescon  26983  cvmliftmolem2  27019  cvmlift2lem12  27051  prodeq2ii  27273  prodmolem2  27295  poseq  27561  ifscgr  27922  cgrxfr  27933  outsideofeu  28009  linethru  28031  fin2so  28260  mblfinlem2  28273  mblfinlem3  28274  itg2addnclem  28287  ftc1anclem7  28317  ftc1anclem8  28318  ftc1anc  28319  neibastop1  28424  ssbnd  28531  totbndbnd  28532  prtlem10  28855  mzpsubst  28930  mzpcompact2lem  28933  eldioph2  28945  eldioph2b  28946  diophren  28997  pell14qrexpcl  29053  elpell1qr2  29058  monotoddzzfi  29128  acongtr  29166  acongrep  29168  jm2.19lem4  29186  jm2.26a  29194  jm2.26lem3  29195  jm2.26  29196  isnumbasgrplem2  29305  mendassa  29396  stoweidlem7  29648  stoweidlem28  29669  stoweidlem34  29675  stoweidlem48  29689  stoweidlem49  29690  stoweidlem52  29693  stoweidlem57  29698  wallispilem3  29708  ralxfrd2  29983  wlkiswwlk1  30170  usg2wotspth  30249  vdiscusgra  30383  vdn1frgrav2  30464  vdgn1frgrav2  30465  frgrancvvdeqlem9  30480  frgrawopreg  30488  frghash2spot  30502  numclwlk1lem2foa  30530  numclwlk1lem2fo  30534  frgrareggt1  30555  4animp1  30902  4an4132  30904  bnj1408  31729  lssats  32230  lkrlss  32313  lshpset2N  32337  2dim  32687  islvol5  32796  paddasslem11  33047  pexmidlem8N  33194  ltrnid  33352  idltrn  33367  trlator0  33388  trlnidatb  33394  cdlemf2  33779  cdlemg2cex  33808  tendodi1  34001  tendodi2  34002  diblss  34388  dihopelvalcpre  34466  dih1dimatlem  34547  dihglblem6  34558
  Copyright terms: Public domain W3C validator