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

Theorem simplll 760
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 455 . 2  |-  ( (
ph  /\  ps )  ->  ph )
21ad2antrr 724 1  |-  ( ( ( ( ph  /\  ps )  /\  ch )  /\  th )  ->  ph )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367
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 369
This theorem is referenced by:  simp-4l  768  f1imass  6152  oeeui  7287  oaabs2  7330  boxcutc  7549  omxpenlem  7655  cantnfle  8121  cantnfleOLD  8151  acndom2  8466  infpwfien  8474  sornom  8688  isf32lem2  8765  isf32lem4  8767  fin1a2lem11  8821  ttukeylem5  8924  pwfseq  9071  gchina  9106  inttsk  9181  inar1  9182  prlem936  9454  mulcmpblnr  9477  00id  9788  mul02lem1  9789  addid1  9793  cnegex  9794  negeu  9845  add20  10104  ltmul12a  10438  lediv12a  10477  cru  10567  qextltlem  11453  xmullem  11508  xlemul1a  11532  ixxss12  11601  ioodisj  11702  elfz0fzfz0  11832  fsuppmapnn0fz  12144  seqf1o  12190  mulexpz  12248  leexp1a  12267  seqcoll  12559  swrdswrdlem  12738  abs3lem  13318  cau3lem  13334  climcau  13640  sumeq2ii  13662  summolem2  13685  climcndslem1  13810  climcndslem2  13811  geomulcvg  13835  mertenslem1  13843  mertenslem2  13844  mertens  13845  prodeq2ii  13870  prodmolem2  13892  bitsfzo  14292  sadadd2lem2  14307  dvdsmulgcd  14399  qredeu  14455  pc2dvds  14609  pcz  14611  ramcl  14754  firest  15045  mreexexlemd  15256  isacs2  15265  iscatd2  15293  ipodrsima  16117  mrelatlub  16138  mndpropd  16268  mhmeql  16317  isgrpinv  16422  mulgnn0dir  16487  mhmid  16513  mhmmnd  16514  issubg4  16542  gasubg  16662  symgextf  16764  pmtr3ncom  16822  gexdvds  16926  oddvdssubg  17183  cyggeninv  17208  cyggenod  17209  issrg  17477  dvdsrmul1  17620  unitgrp  17634  cntzsubr  17779  islmhm2  18002  lmhmeql  18019  lbspropd  18063  lssacsex  18108  issubassa2  18312  mplbas2  18452  mplbas2OLD  18453  psgndiflemA  18933  isphl  18959  ocvocv  18998  lindfmm  19152  scmatmats  19303  smatvscl  19316  mdetdiag  19391  m2cpmfo  19547  pmatcollpw3fi1lem1  19577  pm2mpf1  19590  pm2mpghm  19607  fvmptnn04if  19640  chfacfscmulfsupp  19650  chfacfpmmulfsupp  19654  neissex  19919  neiptoptop  19923  neiptopnei  19924  restbas  19950  tgrest  19951  restopnb  19967  cnpco  20059  isnrm3  20151  isreg2  20169  iuncon  20219  1stcrest  20244  2ndcctbss  20246  2ndcomap  20249  2ndcsep  20250  dislly  20288  kgencn2  20348  ptbasfi  20372  txhaus  20438  txkgen  20443  txcon  20480  qtopcn  20505  regr1lem2  20531  kqnrmlem1  20534  kqnrmlem2  20535  trfbas2  20634  trfil2  20678  flimcf  20773  hauspwpwf1  20778  fclscf  20816  flimfnfcls  20819  cnextcn  20857  ustexsym  21008  ustex2sym  21009  ustex3sym  21010  ustuqtop4  21037  utop3cls  21044  utopreg  21045  ucnima  21074  ucncn  21078  fmucnd  21085  metequiv2  21303  prdsxmslem2  21322  metcnpi3  21339  metusttoOLD  21350  metustto  21351  metustidOLD  21352  metustid  21353  metustexhalfOLD  21356  metustexhalf  21357  ngptgp  21440  xrsblre  21606  icccmp  21620  reconnlem1  21621  reconn  21623  opnreen  21626  metdsf  21642  metdscn  21650  fsumcn  21664  elcncf2  21684  cncfmet  21702  pcoass  21814  lmcau  22041  rrxdstprj1  22126  pmltpc  22152  ivthlem2  22154  ivthlem3  22155  ovollb2  22190  volsup  22256  ioombl1  22262  ioorf  22272  dyadss  22293  dyaddisjlem  22294  dyadmax  22297  volcn  22305  cncombf  22355  mbflimsup  22363  itg2const2  22438  iblss2  22502  cpnord  22628  dvmptfsum  22666  fta1g  22858  plydivex  22983  fta1  22994  aannenlem1  23014  ulmdvlem3  23087  abelthlem8  23124  pilem3  23138  advlogexp  23328  cxpmul2z  23364  atantayl2  23592  jensen  23642  isppw2  23768  lgsqr  24000  lgsdchrval  24001  lgsquad3  24015  2sqb  24032  dchrisumlem3  24055  rpvmasum2  24076  mulog2sumlem2  24099  pntrsumbnd2  24131  f1otrg  24578  f1otrge  24579  axsegcon  24634  axeuclidlem  24669  axcontlem9  24679  eengtrkg  24692  nbgraf1olem5  24849  cusgrasize2inds  24881  0wlkon  24953  0trlon  24954  0pthon  24985  3v3e3cycl2  25068  wlkiswwlk1  25094  usg2wotspth  25288  vdiscusgra  25325  iseupa  25369  vdn1frgrav2  25429  vdgn1frgrav2  25430  frgrancvvdeqlem9  25445  frgrawopreg  25453  frghash2spot  25467  numclwlk1lem2foa  25495  numclwlk1lem2fo  25499  frgrareggt1  25520  vacn  26004  smcnlem  26007  0lno  26105  chocunii  26619  occl  26622  5oalem1  26972  3oalem2  26981  unoplin  27238  hmoplin  27260  lnconi  27351  kbass5  27438  mdslmd1lem1  27643  mdslmd1lem2  27644  mdsymlem2  27722  cdj1i  27751  disjabrex  27860  disjabrexf  27861  acunirnmpt  27929  fgreu  27942  xrge0infss  28008  xrofsup  28016  xrge0addgt0  28119  submomnd  28138  submarchi  28168  archiabllem1  28175  archiabllem2a  28176  isarchiofld  28246  locfinreflem  28282  rge0scvg  28370  lmxrge0  28373  lmdvg  28374  qqhval2  28401  esumrnmpt2  28501  esumfsup  28503  esumpcvgval  28511  esumcvg  28519  esumgect  28523  esumiun  28527  sigaclfu2  28555  sigainb  28570  insiga  28571  fiunelros  28608  measinblem  28654  measinb  28655  measdivcstOLD  28658  measdivcst  28659  omssubadd  28734  oddpwdc  28785  dstrvprob  28902  sgnmul  28973  sgnsub  28975  signsply0  29000  signstfvneq0  29021  bnj1408  29406  ptpcon  29517  sconpi1  29523  rescon  29530  cvmliftmolem2  29566  cvmlift2lem12  29598  poseq  30051  ifscgr  30369  cgrxfr  30380  outsideofeu  30456  linethru  30478  neibastop1  30574  fin2so  31392  mblfinlem2  31404  mblfinlem3  31405  itg2addnclem  31419  ftc1anclem7  31449  ftc1anclem8  31450  ftc1anc  31451  ssbnd  31546  totbndbnd  31547  prtlem10  31868  lssats  32010  lkrlss  32093  lshpset2N  32117  2dim  32467  islvol5  32576  paddasslem11  32827  pexmidlem8N  32974  ltrnid  33132  idltrn  33147  trlator0  33169  trlnidatb  33175  cdlemf2  33561  cdlemg2cex  33590  tendodi1  33783  tendodi2  33784  diblss  34170  dihopelvalcpre  34248  dih1dimatlem  34329  dihglblem6  34340  mzpsubst  35022  mzpcompact2lem  35025  eldioph2  35036  eldioph2b  35037  diophren  35088  pell14qrexpcl  35144  elpell1qr2  35149  monotoddzzfi  35219  acongtr  35257  acongrep  35259  jm2.19lem4  35276  jm2.26a  35284  jm2.26lem3  35285  jm2.26  35286  isnumbasgrplem2  35397  mendassa  35487  prmunb2  36019  4an4132  36265  adant423  36782  mullimc  36971  mullimcf  36978  neglimc  37002  icccncfext  37039  cncfiooicclem1  37045  fprodcncf  37053  dvnprodlem3  37094  iblcncfioo  37126  itgspltprt  37127  stoweidlem7  37138  stoweidlem28  37159  stoweidlem34  37165  stoweidlem48  37179  stoweidlem52  37183  wallispilem3  37198  fourierdlem12  37250  fourierdlem38  37276  fourierdlem39  37277  fourierdlem42  37280  fourierdlem46  37284  fourierdlem48  37286  fourierdlem49  37287  fourierdlem50  37288  fourierdlem51  37289  fourierdlem65  37303  fourierdlem73  37311  fourierdlem76  37314  fourierdlem87  37325  fourierdlem103  37341  fourierdlem104  37342  nnsum4primeseven  37829  nnsum4primesevenALTV  37830  bgoldbtbndlem2  37835  bgoldbtbndlem3  37836  bgoldbtbnd  37838  ralxfrd2  37917  mgmhmeql  38101
  Copyright terms: Public domain W3C validator