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

Theorem simp1d 993
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 981 . 2  |-  ( ( ps  /\  ch  /\  th )  ->  ps )
31, 2syl 16 1  |-  ( ph  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ w3a 958
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  df-3an 960
This theorem is referenced by:  simp1bi  996  f1dom3fv3dif  5967  f1dom3el3dif  5968  oeeui  7029  oeeu  7030  erinxp  7162  domssex2  7459  domssex  7460  cantnflem1a  7881  cantnflem1b  7882  cantnflem1c  7883  cantnflem1d  7884  cantnflem1  7885  cantnflem3  7887  cantnflem4  7888  cantnflem1aOLD  7904  cantnflem1bOLD  7905  cantnflem1cOLD  7906  cantnflem1dOLD  7907  cantnflem1OLD  7908  cantnflem3OLD  7909  cantnflem4OLD  7910  fpwwe2lem7  8791  canthnumlem  8803  canthp1lem2  8808  wuntr  8860  supmul1  10283  supmullem1  10284  supmullem2  10285  supmul  10286  ixxdisj  11303  ixxun  11304  ixxss1  11306  ixxss2  11307  ixxss12  11308  ixxub  11309  ixxlb  11310  iccss2  11354  iocssre  11363  icossre  11364  iccssre  11365  icodisj  11397  iccf1o  11416  xov1plusxeqvd  11418  fzen  11454  intfracq  11682  fldiv  11683  remul  12602  sqrlem6  12721  resqrth  12729  sqrth  12836  ruclem6  13500  ruclem9  13503  ruclem12  13506  gcdn0cl  13681  crt  13836  phimullem  13837  eulerthlem1  13839  eulerthlem2  13840  pcpremul  13893  prmreclem3  13962  sectcan  14677  sectco  14678  sectmon  14699  monsect  14700  funcf1  14759  funcsect  14765  invfuc  14867  coapm  14922  catciso  14958  posref  15104  psrel  15356  pstr  15364  mhmf  15452  submss  15460  eqger  15711  eqgcpbl  15715  gaorber  15806  orbstafun  15809  cayleyth  15900  dprdgrp  16463  dprdff  16470  dprdffOLD  16476  ablfac1a  16544  ablfac1b  16545  lmodvscl  16889  lbsss  17080  2idlcpbl  17238  assalmod  17313  mdetunilem2  18261  mdetunilem5  18264  mdetunilem6  18265  cnptop1  18688  lmfpm  18741  lmff  18747  lmcnp  18750  flimtop  19380  tlmtmd  19603  ustssxp  19621  ustdiag  19625  ustfilxp  19629  ustbas2  19642  tusbas  19685  imasdsf1olem  19790  xmeter  19850  tmsbas  19900  metustexhalfOLD  19980  metustexhalf  19981  nlmngp  20100  qdensere  20191  blcvx  20217  tgqioo  20219  icccmplem2  20242  reconnlem1  20245  cnmpt2pc  20342  icoopnst  20353  iocopnst  20354  iccpnfcnv  20358  phtpcer  20409  phtpcco2  20413  pcohtpylem  20433  pcohtpy  20434  pcopt  20436  pcopt2  20437  pcorevlem  20440  pcorev2  20442  pcophtb  20443  om1addcl  20447  pi1cpbl  20458  pi1grplem  20463  pi1inv  20466  pi1xfrf  20467  pi1xfr  20469  pi1xfrcnvlem  20470  pi1xfrcnv  20471  pi1cof  20473  pi1coghm  20475  cphphl  20532  cphreccllem  20539  cphsqrcl2  20547  tchclm  20589  tchcph  20594  lmcau  20665  bcthlem4  20680  minveclem4c  20754  minveclem2  20755  minveclem3b  20757  minveclem4  20761  minveclem6  20763  ivthicc  20784  ovolfsval  20796  ovollb2lem  20813  ovolshftlem1  20834  ovolscalem1  20838  ovolicc2lem2  20843  ovolicc2lem5  20846  ovolicopnf  20849  ioombl1lem1  20881  ioombl1lem3  20883  ioombl1lem4  20884  uniioovol  20901  uniioombllem2a  20904  uniioombllem2  20905  uniioombllem3a  20906  uniioombllem3  20907  uniioombllem4  20908  uniioombllem6  20910  vitalilem2  20931  vitalilem3  20932  vitalilem4  20933  i1ff  20996  itg2monolem1  21070  itgreval  21116  ibladd  21140  iblabslem  21147  itgspliticc  21156  itgsplitioo  21157  ditgcl  21175  ditgswap  21176  ditgsplitlem  21177  ditgsplit  21178  limcresi  21202  dvlip2  21309  dveq0  21314  dvcnvre  21333  dvfsumlem2  21341  ftc1a  21351  mpfind  21396  ply1rem  21520  facth1  21521  fta1glem1  21522  fta1glem2  21523  ig1pcl  21532  ig1pdvds  21533  plyrem  21656  facth  21657  vieta1lem1  21661  vieta1lem2  21662  aaliou3lem3  21695  aaliou3lem7  21700  pserulm  21772  psercnlem2  21774  psercn  21776  pserdvlem1  21777  pserdvlem2  21778  pserdv  21779  abelth2  21792  coseq00topi  21849  coseq0negpitopi  21850  cosordlem  21872  efif1olem1  21883  dvloglem  21978  loglesqr  22081  quart1  22136  quartlem2  22138  quartlem3  22139  quartlem4  22140  quart  22141  asinsinlem  22171  atanlogsublem  22195  atans2  22211  dvatan  22215  rlimcnp2  22245  divsqrsumlem  22258  ftalem5  22299  ftalem7  22301  basellem4  22306  basellem5  22307  perfectlem2  22454  dchrinv  22485  chpdifbndlem1  22687  pntibndlem2  22725  pntlema  22730  pntlemb  22731  pntlemg  22732  pntlemh  22733  pntlemn  22734  pntlemq  22735  pntlemr  22736  pntlemj  22737  pntlemf  22739  pntlemk  22740  pntlemo  22741  pntlemp  22744  pntleml  22745  abvcxp  22749  axtgbtwnid  22812  cgr3simp1  22853  eupacl  23413  grpofo  23509  vcablo  23758  nvvc  23816  sspba  23948  sspg  23949  minvecolem2  24099  minvecolem4c  24103  minvecolem4  24104  minvecolem5  24105  minvecolem6  24106  eleigveccl  25186  xrofsup  25878  eliccelico  25890  elicoelioo  25891  ogrpaddlt  26005  slmdvscl  26079  slmdvsass  26082  rnlogbval  26313  rnlogbcl  26314  nnlogbexp  26317  logbrec  26318  baselsiga  26412  insiga  26434  measfrge0  26471  sibfmbl  26569  eulerpartlemt  26602  eulerpartlemmf  26606  probfinmeasbOLD  26659  tg5segofs  26845  subfacp1lem2a  26916  subfacp1lem2b  26917  subfacp1lem3  26918  subfacp1lem4  26919  subfacp1lem5  26920  sconpht2  26975  sconpi1  26976  cvxscon  26980  cvmlift2lem3  27042  cvmlift2lem5  27044  cvmlift2lem6  27045  cvmlift2lem7  27046  cvmlift2lem12  27051  cvmliftphtlem  27054  cvmliftpht  27055  cvmlift3lem2  27057  cvmlift3lem4  27059  cvmlift3lem5  27060  cvmlift3lem6  27061  ghomgrplem  27155  iblabsnclem  28299  dvasin  28324  isbnd3  28527  heiborlem3  28556  iccbnd  28583  rngohomf  28616  idlss  28660  stoweidlem30  29671  stoweidlem31  29672  stoweidlem38  29679  stoweidlem44  29685  sigardiv  29743  sigarcol  29746  sharhght  29747  sigaradd  29748  cevathlem1  29749  cevathlem2  29750  cevath  29751  lelttrdi  30024  wwlksubclwwlk  30312  clwwnisshclwwn  30319  rusisusgra  30394  lshplss  32199  opoccl  32412  opococ  32413  oplecon3  32417  hloml  32575  lclkrslem1  34755  lclkrslem2  34756
  Copyright terms: Public domain W3C validator