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

Theorem simplll 759
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  767  f1imass  6157  oeeui  7253  oaabs2  7296  boxcutc  7514  omxpenlem  7620  cantnfle  8093  cantnfleOLD  8123  acndom2  8438  infpwfien  8446  sornom  8660  isf32lem2  8737  isf32lem4  8739  fin1a2lem11  8793  ttukeylem5  8896  pwfseq  9045  gchina  9080  inttsk  9155  inar1  9156  prlem936  9428  mulcmpblnr  9451  00id  9758  mul02lem1  9759  addid1  9763  cnegex  9764  negeu  9815  add20  10071  ltmul12a  10405  lediv12a  10445  cru  10535  qextltlem  11411  xmullem  11466  xlemul1a  11490  ixxss12  11559  ioodisj  11660  elfz0fzfz0  11789  fsuppmapnn0fz  12083  seqf1o  12129  mulexpz  12187  leexp1a  12205  seqcoll  12493  swrdswrdlem  12665  abs3lem  13152  cau3lem  13168  climcau  13474  sumeq2ii  13496  summolem2  13519  climcndslem1  13642  climcndslem2  13643  geomulcvg  13666  mertenslem1  13674  mertenslem2  13675  mertens  13676  prodeq2ii  13701  prodmolem2  13723  bitsfzo  14066  sadadd2lem2  14081  dvdsmulgcd  14173  qredeu  14229  pc2dvds  14383  pcz  14385  ramcl  14528  firest  14811  mreexexlemd  15022  isacs2  15031  iscatd2  15059  ipodrsima  15773  mrelatlub  15794  mndpropd  15924  mhmeql  15973  isgrpinv  16078  mulgnn0dir  16143  mhmid  16169  mhmmnd  16170  issubg4  16198  gasubg  16318  symgextf  16420  pmtr3ncom  16478  gexdvds  16582  oddvdssubg  16839  cyggeninv  16864  cyggenod  16865  issrg  17137  dvdsrmul1  17280  unitgrp  17294  cntzsubr  17439  islmhm2  17662  lmhmeql  17679  lbspropd  17723  lssacsex  17768  issubassa2  17972  mplbas2  18112  mplbas2OLD  18113  psgndiflemA  18614  isphl  18640  ocvocv  18679  lindfmm  18839  scmatmats  18990  smatvscl  19003  mdetdiag  19078  m2cpmfo  19234  pmatcollpw3fi1lem1  19264  pm2mpf1  19277  pm2mpghm  19294  fvmptnn04if  19327  chfacfscmulfsupp  19337  chfacfpmmulfsupp  19341  neissex  19605  neiptoptop  19609  neiptopnei  19610  restbas  19636  tgrest  19637  restopnb  19653  cnpco  19745  isnrm3  19837  isreg2  19855  iuncon  19906  1stcrest  19931  2ndcctbss  19933  2ndcomap  19936  2ndcsep  19937  dislly  19975  kgencn2  20035  ptbasfi  20059  txhaus  20125  txkgen  20130  txcon  20167  qtopcn  20192  regr1lem2  20218  kqnrmlem1  20221  kqnrmlem2  20222  trfbas2  20321  trfil2  20365  flimcf  20460  hauspwpwf1  20465  fclscf  20503  flimfnfcls  20506  cnextcn  20544  ustexsym  20695  ustex2sym  20696  ustex3sym  20697  ustuqtop4  20724  utop3cls  20731  utopreg  20732  ucnima  20761  ucncn  20765  fmucnd  20772  metequiv2  20990  prdsxmslem2  21009  metcnpi3  21026  metusttoOLD  21037  metustto  21038  metustidOLD  21039  metustid  21040  metustexhalfOLD  21043  metustexhalf  21044  ngptgp  21127  xrsblre  21293  icccmp  21307  reconnlem1  21308  reconn  21310  opnreen  21313  metdsf  21329  metdscn  21337  fsumcn  21351  elcncf2  21371  cncfmet  21389  pcoass  21501  lmcau  21728  rrxdstprj1  21813  pmltpc  21839  ivthlem2  21841  ivthlem3  21842  ovollb2  21877  volsup  21943  ioombl1  21949  ioorf  21959  dyadss  21980  dyaddisjlem  21981  dyadmax  21984  volcn  21992  cncombf  22042  mbflimsup  22050  itg2const2  22125  iblss2  22189  cpnord  22315  dvmptfsum  22353  fta1g  22545  plydivex  22669  fta1  22680  aannenlem1  22700  ulmdvlem3  22773  abelthlem8  22810  pilem3  22824  advlogexp  23012  cxpmul2z  23048  atantayl2  23245  jensen  23294  isppw2  23365  lgsqr  23597  lgsdchrval  23598  lgsquad3  23612  2sqb  23629  dchrisumlem3  23652  rpvmasum2  23673  mulog2sumlem2  23696  pntrsumbnd2  23728  f1otrg  24150  f1otrge  24151  axsegcon  24206  axeuclidlem  24241  axcontlem9  24251  eengtrkg  24264  nbgraf1olem5  24421  cusgrasize2inds  24453  0wlkon  24525  0trlon  24526  0pthon  24557  3v3e3cycl2  24640  wlkiswwlk1  24666  usg2wotspth  24860  vdiscusgra  24897  iseupa  24941  vdn1frgrav2  25001  vdgn1frgrav2  25002  frgrancvvdeqlem9  25017  frgrawopreg  25025  frghash2spot  25039  numclwlk1lem2foa  25067  numclwlk1lem2fo  25071  frgrareggt1  25092  vacn  25580  smcnlem  25583  0lno  25681  chocunii  26195  occl  26198  5oalem1  26548  3oalem2  26557  unoplin  26815  hmoplin  26837  lnconi  26928  kbass5  27015  mdslmd1lem1  27220  mdslmd1lem2  27221  mdsymlem2  27299  cdj1i  27328  disjabrex  27419  disjabrexf  27420  fgreu  27489  xrge0infss  27556  xrofsup  27558  xrge0addgt0  27658  submomnd  27677  submarchi  27707  archiabllem1  27714  archiabllem2a  27715  isarchiofld  27784  locfinreflem  27820  rge0scvg  27908  lmxrge0  27911  lmdvg  27912  qqhval2  27940  esumfsup  28053  esumpcvgval  28061  esumcvg  28069  sigaclfu2  28098  sigainb  28113  insiga  28114  measinblem  28168  measinb  28169  measdivcstOLD  28172  measdivcst  28173  oddpwdc  28270  dstrvprob  28387  sgnmul  28458  sgnsub  28460  signsply0  28485  signstfvneq0  28506  ptpcon  28655  sconpi1  28661  rescon  28668  cvmliftmolem2  28704  cvmlift2lem12  28736  poseq  29308  ifscgr  29669  cgrxfr  29680  outsideofeu  29756  linethru  29778  fin2so  30015  mblfinlem2  30027  mblfinlem3  30028  itg2addnclem  30041  ftc1anclem7  30071  ftc1anclem8  30072  ftc1anc  30073  neibastop1  30152  ssbnd  30259  totbndbnd  30260  prtlem10  30581  mzpsubst  30656  mzpcompact2lem  30659  eldioph2  30670  eldioph2b  30671  diophren  30722  pell14qrexpcl  30778  elpell1qr2  30783  monotoddzzfi  30853  acongtr  30891  acongrep  30893  jm2.19lem4  30909  jm2.26a  30917  jm2.26lem3  30918  jm2.26  30919  isnumbasgrplem2  31028  mendassa  31119  prmunb2  31167  adant423  31379  mullimc  31530  mullimcf  31537  neglimc  31561  icccncfext  31597  cncfiooicclem1  31603  iblcncfioo  31667  itgspltprt  31668  stoweidlem7  31678  stoweidlem28  31699  stoweidlem34  31705  stoweidlem48  31719  stoweidlem52  31723  wallispilem3  31738  fourierdlem12  31790  fourierdlem38  31816  fourierdlem39  31817  fourierdlem42  31820  fourierdlem46  31824  fourierdlem48  31826  fourierdlem49  31827  fourierdlem50  31828  fourierdlem51  31829  fourierdlem65  31843  fourierdlem73  31851  fourierdlem76  31854  fourierdlem87  31865  fourierdlem103  31881  fourierdlem104  31882  ralxfrd2  32141  mgmhmeql  32329  4an4132  33001  bnj1408  33825  lssats  34477  lkrlss  34560  lshpset2N  34584  2dim  34934  islvol5  35043  paddasslem11  35294  pexmidlem8N  35441  ltrnid  35599  idltrn  35614  trlator0  35636  trlnidatb  35642  cdlemf2  36028  cdlemg2cex  36057  tendodi1  36250  tendodi2  36251  diblss  36637  dihopelvalcpre  36715  dih1dimatlem  36796  dihglblem6  36807
  Copyright terms: Public domain W3C validator