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

Theorem simplll 773
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 463 . 2  |-  ( (
ph  /\  ps )  ->  ph )
21ad2antrr 737 1  |-  ( ( ( ( ph  /\  ps )  /\  ch )  /\  th )  ->  ph )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 375
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 190  df-an 377
This theorem is referenced by:  simp-4l  781  f1imass  6195  oeeui  7334  oaabs2  7377  boxcutc  7596  omxpenlem  7704  cantnfle  8207  acndom2  8516  infpwfien  8524  sornom  8738  isf32lem2  8815  isf32lem4  8817  fin1a2lem11  8871  ttukeylem5  8974  pwfseq  9120  gchina  9155  inttsk  9230  inar1  9231  prlem936  9503  mulcmpblnr  9526  00id  9839  mul02lem1  9840  addid1  9844  cnegex  9845  negeu  9896  add20  10159  ltmul12a  10494  lediv12a  10532  fiminre  10588  cru  10634  qextltlem  11529  xmullem  11584  xlemul1a  11608  ixxss12  11689  ioodisj  11797  elfz0fzfz0  11931  fsuppmapnn0fz  12246  seqf1o  12292  mulexpz  12350  leexp1a  12369  seqcoll  12666  swrdswrdlem  12858  abs3lem  13456  cau3lem  13472  climcau  13789  sumeq2ii  13814  summolem2  13837  climcndslem1  13962  climcndslem2  13963  geomulcvg  13987  mertenslem1  13995  mertenslem2  13996  mertens  13997  prodeq2ii  14022  prodmolem2  14044  bitsfzo  14464  sadadd2lem2  14479  dvdsmulgcd  14577  qredeu  14719  pc2dvds  14883  pcz  14885  ramcl  15042  firest  15386  mreexexlemd  15605  isacs2  15614  iscatd2  15642  ipodrsima  16466  mrelatlub  16487  mndpropd  16617  mhmeql  16666  isgrpinv  16771  mulgnn0dir  16836  mhmid  16862  mhmmnd  16863  issubg4  16891  gasubg  17011  symgextf  17113  pmtr3ncom  17171  gexdvds  17290  oddvdssubg  17548  cyggeninv  17573  cyggenod  17574  issrg  17796  dvdsrmul1  17936  unitgrp  17950  cntzsubr  18095  islmhm2  18316  lmhmeql  18333  lbspropd  18377  lssacsex  18422  issubassa2  18624  mplbas2  18749  psgndiflemA  19224  isphl  19250  ocvocv  19289  lindfmm  19440  scmatmats  19591  smatvscl  19604  mdetdiag  19679  m2cpmfo  19835  pmatcollpw3fi1lem1  19865  pm2mpf1  19878  pm2mpghm  19895  fvmptnn04if  19928  chfacfscmulfsupp  19938  chfacfpmmulfsupp  19942  neissex  20198  neiptoptop  20202  neiptopnei  20203  restbas  20229  tgrest  20230  restopnb  20246  cnpco  20338  isnrm3  20430  isreg2  20448  iuncon  20498  1stcrest  20523  2ndcctbss  20525  2ndcomap  20528  2ndcsep  20529  dislly  20567  kgencn2  20627  ptbasfi  20651  txhaus  20717  txkgen  20722  txcon  20759  qtopcn  20784  regr1lem2  20810  kqnrmlem1  20813  kqnrmlem2  20814  trfbas2  20913  trfil2  20957  flimcf  21052  hauspwpwf1  21057  fclscf  21095  flimfnfcls  21098  cnextcn  21137  ustexsym  21285  ustex2sym  21286  ustex3sym  21287  ustuqtop4  21314  utop3cls  21321  utopreg  21322  ucnima  21351  ucncn  21355  fmucnd  21362  metequiv2  21580  prdsxmslem2  21599  metcnpi3  21616  metustto  21623  metustid  21624  metustexhalf  21626  ngptgp  21699  xrsblre  21884  icccmp  21898  reconnlem1  21899  reconn  21901  opnreen  21904  metdsf  21920  metdscn  21928  metdsfOLD  21935  metdscnOLD  21943  fsumcn  21957  elcncf2  21977  cncfmet  21995  pcoass  22110  lmcau  22337  rrxdstprj1  22418  pmltpc  22456  ivthlem2  22458  ivthlem3  22459  ovollb2  22497  volsup  22565  ioombl1  22571  ioorf  22581  ioorfOLD  22586  dyadss  22608  dyaddisjlem  22609  dyadmax  22612  volcn  22620  cncombf  22670  mbflimsup  22679  mbflimsupOLD  22680  itg2const2  22755  iblss2  22819  cpnord  22945  dvmptfsum  22983  fta1g  23174  plydivex  23306  fta1  23317  aannenlem1  23340  ulmdvlem3  23413  abelthlem8  23450  pilem3  23465  pilem3OLD  23466  advlogexp  23656  cxpmul2z  23692  atantayl2  23920  jensen  23970  isppw2  24098  lgsqr  24330  lgsdchrval  24331  lgsquad3  24345  2sqb  24362  dchrisumlem3  24385  rpvmasum2  24406  mulog2sumlem2  24429  pntrsumbnd2  24461  f1otrg  24957  f1otrge  24958  axsegcon  25013  axeuclidlem  25048  axcontlem9  25058  eengtrkg  25071  nbgraf1olem5  25229  cusgrasize2inds  25261  0wlkon  25333  0trlon  25334  0pthon  25365  3v3e3cycl2  25448  wlkiswwlk1  25474  usg2wotspth  25668  vdiscusgra  25705  iseupa  25749  vdn1frgrav2  25809  vdgn1frgrav2  25810  frgrancvvdeqlem9  25825  frgrawopreg  25833  frghash2spot  25847  numclwlk1lem2foa  25875  numclwlk1lem2fo  25879  frgrareggt1  25900  vacn  26386  smcnlem  26389  0lno  26487  chocunii  27010  occl  27013  5oalem1  27363  3oalem2  27372  unoplin  27629  hmoplin  27651  lnconi  27742  kbass5  27829  mdslmd1lem1  28034  mdslmd1lem2  28035  mdsymlem2  28113  cdj1i  28142  disjabrex  28246  disjabrexf  28247  acunirnmpt  28313  fgreu  28326  xrge0infss  28392  xrge0infssOLD  28393  xrofsup  28405  xrge0addgt0  28505  submomnd  28524  submarchi  28554  archiabllem1  28561  archiabllem2a  28562  isarchiofld  28631  locfinreflem  28718  rge0scvg  28806  lmxrge0  28809  lmdvg  28810  qqhval2  28837  esumrnmpt2  28940  esumfsup  28942  esumpcvgval  28950  esumcvg  28958  esumgect  28962  esumiun  28966  sigaclfu2  28994  sigainb  29009  insiga  29010  fiunelros  29047  measinblem  29093  measinb  29094  measdivcstOLD  29097  measdivcst  29098  omssubadd  29178  omssubaddOLD  29182  oddpwdc  29237  dstrvprob  29354  sgnmul  29463  sgnsub  29465  signsply0  29490  signstfvneq0  29511  bnj1408  29895  ptpcon  30006  sconpi1  30012  rescon  30019  cvmliftmolem2  30055  cvmlift2lem12  30087  poseq  30541  ifscgr  30861  cgrxfr  30872  outsideofeu  30948  linethru  30970  neibastop1  31065  fin2so  31978  poimirlem28  32014  poimirlem31  32017  mblfinlem2  32024  mblfinlem3  32025  itg2addnclem  32039  ftc1anclem7  32069  ftc1anclem8  32070  ftc1anc  32071  ssbnd  32166  totbndbnd  32167  prtlem10  32483  lssats  32624  lkrlss  32707  lshpset2N  32731  2dim  33081  islvol5  33190  paddasslem11  33441  pexmidlem8N  33588  ltrnid  33746  idltrn  33761  trlator0  33783  trlnidatb  33789  cdlemf2  34175  cdlemg2cex  34204  tendodi1  34397  tendodi2  34398  diblss  34784  dihopelvalcpre  34862  dih1dimatlem  34943  dihglblem6  34954  mzpsubst  35636  mzpcompact2lem  35639  eldioph2  35650  eldioph2b  35651  diophren  35702  pell14qrexpcl  35759  elpell1qr2  35764  monotoddzzfi  35836  acongtr  35874  acongrep  35876  jm2.19lem4  35893  jm2.26a  35901  jm2.26lem3  35902  jm2.26  35903  isnumbasgrplem2  36009  mendassa  36106  prmunb2  36704  4an4132  36900  adant423  37408  fiiuncl  37445  supxrgelem  37635  infxr  37666  mullimc  37782  mullimcf  37789  neglimc  37814  icccncfext  37851  cncfiooicclem1  37857  fprodcncf  37865  dvnprodlem3  37909  iblcncfioo  37941  itgspltprt  37942  stoweidlem7  37968  stoweidlem28  37989  stoweidlem34  37996  stoweidlem48  38010  stoweidlem52  38014  wallispilem3  38030  fourierdlem12  38082  fourierdlem38  38109  fourierdlem39  38110  fourierdlem42  38113  fourierdlem42OLD  38114  fourierdlem46  38117  fourierdlem48  38119  fourierdlem49  38120  fourierdlem50  38121  fourierdlem51  38122  fourierdlem65  38136  fourierdlem73  38144  fourierdlem76  38147  fourierdlem87  38158  fourierdlem103  38174  fourierdlem104  38175  sge0f1o  38327  sge0le  38352  ismeannd  38410  isomenndlem  38459  hoicvr  38477  hoidmvle  38529  nnsum4primeseven  39030  nnsum4primesevenALTV  39031  bgoldbtbndlem2  39036  bgoldbtbndlem3  39037  bgoldbtbnd  39039  ralxfrd2  39144  cusgrsize2inds  39660  usgr2wlkneq  39884  umgr3v3e3cycl  40021  mgmhmeql  40172
  Copyright terms: Public domain W3C validator