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

Theorem simp1d 1006
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 994 . 2  |-  ( ( ps  /\  ch  /\  th )  ->  ps )
31, 2syl 16 1  |-  ( ph  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ w3a 971
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  df-3an 973
This theorem is referenced by:  simp1bi  1009  f1dom3fv3dif  6150  f1dom3el3dif  6151  oeeui  7243  oeeu  7244  erinxp  7377  domssex2  7670  domssex  7671  cantnflem1a  8095  cantnflem1b  8096  cantnflem1c  8097  cantnflem1d  8098  cantnflem1  8099  cantnflem3  8101  cantnflem4  8102  cantnflem1aOLD  8118  cantnflem1bOLD  8119  cantnflem1cOLD  8120  cantnflem1dOLD  8121  cantnflem1OLD  8122  cantnflem3OLD  8123  cantnflem4OLD  8124  fpwwe2lem7  9003  canthnumlem  9015  canthp1lem2  9020  wuntr  9072  supmul1  10503  supmullem1  10504  supmullem2  10505  supmul  10506  ixxdisj  11547  ixxun  11548  ixxss1  11550  ixxss2  11551  ixxss12  11552  ixxub  11553  ixxlb  11554  iccss2  11598  iocssre  11607  icossre  11608  iccssre  11609  icodisj  11648  iccf1o  11667  xov1plusxeqvd  11669  fzen  11706  intfracq  11968  fldiv  11969  remul  13047  sqrlem6  13166  resqrtth  13174  sqrtth  13282  ruclem6  14055  ruclem9  14058  ruclem12  14061  gcdn0cl  14239  crt  14395  phimullem  14396  eulerthlem1  14398  eulerthlem2  14399  pcpremul  14454  prmreclem3  14523  sectcan  15246  sectco  15247  sectmon  15273  monsect  15274  funcf1  15357  funcsect  15363  invfuc  15465  coapm  15552  catciso  15588  posrefOLD  15783  psrel  16035  pstr  16043  mhmf  16173  submss  16183  eqger  16453  eqgcpbl  16457  gaorber  16548  orbstafun  16551  cayleyth  16642  dprdgrp  17236  dprdff  17244  dprdffOLD  17250  ablfac1a  17318  ablfac1b  17319  lmodvscl  17727  lbsss  17921  2idlcpbl  18080  assalmod  18166  mpfind  18403  mdetunilem2  19285  mdetunilem5  19288  mdetunilem6  19289  chfacfisfcpmat  19526  cnptop1  19913  lmfpm  19966  lmff  19972  lmcnp  19975  flimtop  20635  tlmtmd  20858  ustssxp  20876  ustdiag  20880  ustfilxp  20884  ustbas2  20897  tusbas  20940  imasdsf1olem  21045  xmeter  21105  tmsbas  21155  metustexhalfOLD  21235  metustexhalf  21236  nlmngp  21355  qdensere  21446  blcvx  21472  tgqioo  21474  icccmplem2  21497  reconnlem1  21500  cnmpt2pc  21597  icoopnst  21608  iocopnst  21609  iccpnfcnv  21613  phtpcer  21664  phtpcco2  21668  pcohtpylem  21688  pcohtpy  21689  pcopt  21691  pcopt2  21692  pcorevlem  21695  pcorev2  21697  pcophtb  21698  om1addcl  21702  pi1cpbl  21713  pi1grplem  21718  pi1inv  21721  pi1xfrf  21722  pi1xfr  21724  pi1xfrcnvlem  21725  pi1xfrcnv  21726  pi1cof  21728  pi1coghm  21730  cphphl  21787  cphreccllem  21794  cphsqrtcl2  21802  tchclm  21844  tchcph  21849  lmcau  21920  bcthlem4  21935  minveclem4c  22009  minveclem2  22010  minveclem3b  22012  minveclem4  22016  minveclem6  22018  ivthicc  22039  ovolfsval  22051  ovollb2lem  22068  ovolshftlem1  22089  ovolscalem1  22093  ovolicc2lem2  22098  ovolicc2lem5  22101  ovolicopnf  22104  ioombl1lem1  22137  ioombl1lem3  22139  ioombl1lem4  22140  uniioovol  22157  uniioombllem2a  22160  uniioombllem2  22161  uniioombllem3a  22162  uniioombllem3  22163  uniioombllem4  22164  uniioombllem6  22166  vitalilem2  22187  vitalilem3  22188  vitalilem4  22189  i1ff  22252  itg2monolem1  22326  itgreval  22372  ibladd  22396  iblabslem  22403  itgspliticc  22412  itgsplitioo  22413  ditgcl  22431  ditgswap  22432  ditgsplitlem  22433  ditgsplit  22434  limcresi  22458  dvlip2  22565  dveq0  22570  dvcnvre  22589  dvfsumlem2  22597  ftc1a  22607  ply1rem  22733  facth1  22734  fta1glem1  22735  fta1glem2  22736  ig1pcl  22745  ig1pdvds  22746  plyrem  22870  facth  22871  vieta1lem1  22875  vieta1lem2  22876  aaliou3lem3  22909  aaliou3lem7  22914  pserulm  22986  psercnlem2  22988  psercn  22990  pserdvlem1  22991  pserdvlem2  22992  pserdv  22993  abelth2  23006  coseq00topi  23064  coseq0negpitopi  23065  cosordlem  23087  efif1olem1  23098  dvloglem  23200  loglesqrt  23303  relogbval  23314  nnlogbexp  23323  logbrec  23324  quart1  23387  quartlem2  23389  quartlem3  23390  quartlem4  23391  quart  23392  asinsinlem  23422  atanlogsublem  23446  atans2  23462  dvatan  23466  rlimcnp2  23497  divsqrtsumlem  23510  ftalem5  23551  ftalem7  23553  basellem4  23558  basellem5  23559  perfectlem2  23706  dchrinv  23737  chpdifbndlem1  23939  pntibndlem2  23977  pntlema  23982  pntlemb  23983  pntlemg  23984  pntlemh  23985  pntlemn  23986  pntlemq  23987  pntlemr  23988  pntlemj  23989  pntlemf  23991  pntlemk  23992  pntlemo  23993  pntlemp  23996  pntleml  23997  abvcxp  24001  axtgbtwnid  24064  cgr3simp1  24115  hlne1  24193  hltr  24198  btwnhl  24202  mirhl  24263  opphllem4  24326  wwlksubclwwlk  25009  clwwnisshclwwn  25014  rusisusgra  25136  eupacl  25174  grpofo  25402  vcablo  25651  nvvc  25709  sspba  25841  sspg  25842  minvecolem2  25992  minvecolem4c  25996  minvecolem4  25997  minvecolem5  25998  minvecolem6  25999  eleigveccl  27079  xrofsup  27819  eliccelico  27825  elicoelioo  27826  slmdvscl  27994  slmdvsass  27997  baselsiga  28348  insiga  28370  sigapildsys  28391  measfrge0  28414  sibfmbl  28544  eulerpartlemt  28577  eulerpartlemmf  28581  probfinmeasbOLD  28634  tg5segofs  28820  subfacp1lem2a  28891  subfacp1lem2b  28892  subfacp1lem3  28893  subfacp1lem4  28894  subfacp1lem5  28895  sconpht2  28950  sconpi1  28951  cvxscon  28955  cvmlift2lem3  29017  cvmlift2lem5  29019  cvmlift2lem6  29020  cvmlift2lem7  29021  cvmlift2lem12  29026  cvmliftphtlem  29029  cvmliftpht  29030  cvmlift3lem2  29032  cvmlift3lem4  29034  cvmlift3lem5  29035  cvmlift3lem6  29036  msrf  29169  elmsta  29175  mthmpps  29209  mclsppslem  29210  mclspps  29211  ghomgrplem  29296  iblabsnclem  30321  dvasin  30346  isbnd3  30523  heiborlem3  30552  iccbnd  30579  rngohomf  30612  idlss  30656  eliccre  31782  eliocre  31789  icoiccdif  31806  limccog  31868  lptioo1  31880  cncfiooicclem1  31938  cncfioobdlem  31941  ditgeqiooicc  32001  stoweidlem30  32054  stoweidlem31  32055  stoweidlem38  32062  stoweidlem44  32068  fourierdlem26  32157  fourierdlem32  32163  fourierdlem33  32164  fourierdlem37  32168  fourierdlem42  32173  fourierdlem54  32185  fourierdlem63  32194  fourierdlem64  32195  fourierdlem65  32196  fourierdlem69  32200  fourierdlem79  32210  fourierdlem82  32213  fourierdlem89  32220  fourierdlem90  32221  fourierdlem91  32222  fourierdlem111  32242  sigardiv  32320  sigarcol  32323  sharhght  32324  sigaradd  32325  cevathlem1  32326  cevathlem2  32327  cevath  32328  perfectALTVlem2  32616  proththd  32620  lelttrdi  32716  lshplss  35122  opoccl  35335  opococ  35336  oplecon3  35340  hloml  35498  lclkrslem1  37680  lclkrslem2  37681
  Copyright terms: Public domain W3C validator