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

Theorem simp1d 1017
Description: Deduce a conjunct from a triple conjunction. (Contributed by NM, 4-Sep-2005.)
Hypothesis
Ref Expression
3simp1d.1  |-  ( ph  ->  ( ps  /\  ch  /\ 
th ) )
Assertion
Ref Expression
simp1d  |-  ( ph  ->  ps )

Proof of Theorem simp1d
StepHypRef Expression
1 3simp1d.1 . 2  |-  ( ph  ->  ( ps  /\  ch  /\ 
th ) )
2 simp1 1005 . 2  |-  ( ( ps  /\  ch  /\  th )  ->  ps )
31, 2syl 17 1  |-  ( ph  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ w3a 982
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 188  df-an 372  df-3an 984
This theorem is referenced by:  simp1bi  1020  f1dom3fv3dif  6120  f1dom3el3dif  6121  f1prex  6134  oeeui  7251  oeeu  7252  erinxp  7385  domssex2  7678  domssex  7679  cantnflem1a  8135  cantnflem1b  8136  cantnflem1c  8137  cantnflem1d  8138  cantnflem1  8139  cantnflem3  8141  cantnflem4  8142  fpwwe2lem7  9005  canthnumlem  9017  canthp1lem2  9022  wuntr  9074  supmul1  10520  supmullem1  10521  supmullem2  10522  supmul  10523  ixxdisj  11594  ixxun  11595  ixxss1  11597  ixxss2  11598  ixxss12  11599  ixxub  11600  ixxlb  11601  ixxlbOLD  11602  iccss2  11649  iocssre  11658  icossre  11659  iccssre  11660  icodisj  11701  iccf1o  11720  xov1plusxeqvd  11722  fzen  11760  intfracq  12029  fldiv  12030  remul  13129  sqrlem6  13248  resqrtth  13256  sqrtth  13364  ruclem6  14223  ruclem9  14226  ruclem12  14229  gcdn0cl  14412  crt  14662  phimullem  14663  eulerthlem1  14665  eulerthlem2  14666  pcpremul  14729  prmreclem3  14798  sectcan  15596  sectco  15597  sectmon  15623  monsect  15624  funcf1  15707  funcsect  15713  invfuc  15815  coapm  15902  catciso  15938  posrefOLD  16133  psrel  16385  pstr  16393  mhmf  16523  submss  16533  eqger  16803  eqgcpbl  16807  gaorber  16898  orbstafun  16901  cayleyth  16992  dprdgrp  17573  dprdff  17581  ablfac1a  17638  ablfac1b  17639  lmodvscl  18044  lbsss  18236  2idlcpbl  18394  assalmod  18479  mpfind  18695  mdetunilem2  19573  mdetunilem5  19576  mdetunilem6  19577  chfacfisfcpmat  19814  cnptop1  20193  lmfpm  20246  lmff  20252  lmcnp  20255  flimtop  20915  tlmtmd  21136  ustssxp  21154  ustdiag  21158  ustfilxp  21162  ustbas2  21175  tusbas  21218  imasdsf1olem  21323  xmeter  21383  tmsbas  21433  metustexhalf  21506  nlmngp  21615  qdensere  21725  blcvx  21751  tgqioo  21753  icccmplem2  21776  reconnlem1  21779  cnmpt2pc  21891  icoopnst  21902  iocopnst  21903  iccpnfcnv  21907  phtpcer  21961  phtpcco2  21965  pcohtpylem  21985  pcohtpy  21986  pcopt  21988  pcopt2  21989  pcorevlem  21992  pcorev2  21994  pcophtb  21995  om1addcl  21999  pi1cpbl  22010  pi1grplem  22015  pi1inv  22018  pi1xfrf  22019  pi1xfr  22021  pi1xfrcnvlem  22022  pi1xfrcnv  22023  pi1cof  22025  pi1coghm  22027  cphphl  22084  cphreccllem  22091  cphsqrtcl2  22099  tchclm  22141  tchcph  22146  lmcau  22217  bcthlem4  22230  minveclem4c  22302  minveclem2  22303  minveclem3b  22305  minveclem4  22309  minveclem6  22311  minveclem4cOLD  22314  minveclem2OLD  22315  minveclem3bOLD  22317  minveclem4OLD  22321  minveclem6OLD  22323  ivthicc  22344  ovolfsval  22358  ovollb2lem  22376  ovolshftlem1  22397  ovolscalem1  22401  ovolicc2lem2  22406  ovolicc2lem5  22410  ovolicopnf  22413  ioombl1lem1  22446  ioombl1lem3  22448  ioombl1lem4  22449  uniioovol  22471  uniioombllem2a  22474  uniioombllem2  22475  uniioombllem2OLD  22476  uniioombllem3a  22477  uniioombllem3  22478  uniioombllem4  22479  uniioombllem6  22481  vitalilem2  22502  vitalilem3  22503  vitalilem4  22504  i1ff  22569  itg2monolem1  22643  itgreval  22689  ibladd  22713  iblabslem  22720  itgspliticc  22729  itgsplitioo  22730  ditgcl  22748  ditgswap  22749  ditgsplitlem  22750  ditgsplit  22751  limcresi  22775  dvlip2  22882  dveq0  22887  dvcnvre  22906  dvfsumlem2  22914  ftc1a  22924  ply1rem  23049  facth1  23050  fta1glem1  23051  fta1glem2  23052  ig1pcl  23062  ig1pdvds  23063  ig1pclOLD  23068  ig1pdvdsOLD  23069  plyrem  23193  facth  23194  vieta1lem1  23198  vieta1lem2  23199  aaliou3lem3  23235  aaliou3lem7  23240  pserulm  23312  psercnlem2  23314  psercn  23316  pserdvlem1  23317  pserdvlem2  23318  pserdv  23319  abelth2  23332  coseq00topi  23392  coseq0negpitopi  23393  cosordlem  23415  efif1olem1  23426  dvloglem  23528  loglesqrt  23633  relogbval  23644  nnlogbexp  23653  logbrec  23654  quart1  23717  quartlem2  23719  quartlem3  23720  quartlem4  23721  quart  23722  asinsinlem  23752  atanlogsublem  23776  atans2  23792  dvatan  23796  rlimcnp2  23827  divsqrtsumlem  23840  ftalem5  23936  ftalem5OLD  23938  ftalem7  23940  basellem4  23945  basellem5  23946  perfectlem2  24093  dchrinv  24124  chpdifbndlem1  24326  pntibndlem2  24364  pntlema  24369  pntlemb  24370  pntlemg  24371  pntlemh  24372  pntlemn  24373  pntlemq  24374  pntlemr  24375  pntlemj  24376  pntlemf  24378  pntlemk  24379  pntlemo  24380  pntlemp  24383  pntleml  24384  abvcxp  24388  axtgbtwnid  24449  cgr3simp1  24500  hlne1  24585  hltr  24590  btwnhl  24594  mirhl  24659  opphllem4  24727  hlpasch  24733  inagswap  24815  wwlksubclwwlk  25467  clwwnisshclwwn  25472  rusisusgra  25594  eupacl  25632  grpofo  25862  vcablo  26111  nvvc  26169  sspba  26301  sspg  26302  minvecolem2  26452  minvecolem4c  26456  minvecolem4  26457  minvecolem5  26458  minvecolem6  26459  minvecolem2OLD  26462  minvecolem4cOLD  26466  minvecolem4OLD  26467  minvecolem5OLD  26468  minvecolem6OLD  26469  eleigveccl  27547  xrofsup  28296  eliccelico  28302  elicoelioo  28303  slmdvscl  28474  slmdvsass  28477  baselsiga  28882  insiga  28904  ldsysgenld  28927  sigapildsys  28929  ldgenpisyslem1  28930  measfrge0  28970  sibfmbl  29113  eulerpartlemt  29149  eulerpartlemmf  29153  probfinmeasbOLD  29206  tg5segofs  29435  subfacp1lem2a  29848  subfacp1lem2b  29849  subfacp1lem3  29850  subfacp1lem4  29851  subfacp1lem5  29852  sconpht2  29906  sconpi1  29907  cvxscon  29911  cvmlift2lem3  29973  cvmlift2lem5  29975  cvmlift2lem6  29976  cvmlift2lem7  29977  cvmlift2lem12  29982  cvmliftphtlem  29985  cvmliftpht  29986  cvmlift3lem2  29988  cvmlift3lem4  29990  cvmlift3lem5  29991  cvmlift3lem6  29992  msrf  30125  elmsta  30131  mthmpps  30165  mclsppslem  30166  mclspps  30167  ghomgrplem  30252  iblabsnclem  31906  dvasin  31929  isbnd3  32017  heiborlem3  32046  iccbnd  32073  rngohomf  32106  idlss  32150  lshplss  32453  opoccl  32666  opococ  32667  oplecon3  32671  hloml  32829  lclkrslem1  35011  lclkrslem2  35012  eliccre  37489  eliocre  37495  icoiccdif  37511  limccog  37577  lptioo1  37589  cncfiooicclem1  37648  cncfioobdlem  37651  ditgeqiooicc  37714  stoweidlem30  37768  stoweidlem31  37769  stoweidlem38  37776  stoweidlem44  37782  fourierdlem26  37872  fourierdlem32  37879  fourierdlem33  37880  fourierdlem37  37884  fourierdlem42  37889  fourierdlem42OLD  37890  fourierdlem54  37901  fourierdlem63  37910  fourierdlem64  37911  fourierdlem65  37912  fourierdlem69  37916  fourierdlem79  37926  fourierdlem82  37929  fourierdlem89  37936  fourierdlem90  37937  fourierdlem91  37938  fourierdlem111  37958  0sal  38039  hoidmv1lelem3  38256  sigardiv  38278  sigarcol  38281  sharhght  38282  sigaradd  38283  cevathlem1  38284  cevathlem2  38285  cevath  38286  perfectALTVlem2  38651  proththd  38721  lelttrdi  38838
  Copyright terms: Public domain W3C validator