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

Theorem simp1d 1000
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 988 . 2  |-  ( ( ps  /\  ch  /\  th )  ->  ps )
31, 2syl 16 1  |-  ( ph  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ w3a 965
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 967
This theorem is referenced by:  simp1bi  1003  f1dom3fv3dif  6090  f1dom3el3dif  6091  oeeui  7152  oeeu  7153  erinxp  7285  domssex2  7582  domssex  7583  cantnflem1a  8005  cantnflem1b  8006  cantnflem1c  8007  cantnflem1d  8008  cantnflem1  8009  cantnflem3  8011  cantnflem4  8012  cantnflem1aOLD  8028  cantnflem1bOLD  8029  cantnflem1cOLD  8030  cantnflem1dOLD  8031  cantnflem1OLD  8032  cantnflem3OLD  8033  cantnflem4OLD  8034  fpwwe2lem7  8915  canthnumlem  8927  canthp1lem2  8932  wuntr  8984  supmul1  10407  supmullem1  10408  supmullem2  10409  supmul  10410  ixxdisj  11427  ixxun  11428  ixxss1  11430  ixxss2  11431  ixxss12  11432  ixxub  11433  ixxlb  11434  iccss2  11478  iocssre  11487  icossre  11488  iccssre  11489  icodisj  11528  iccf1o  11547  xov1plusxeqvd  11549  fzen  11585  intfracq  11816  fldiv  11817  remul  12737  sqrlem6  12856  resqrth  12864  sqrth  12971  ruclem6  13636  ruclem9  13639  ruclem12  13642  gcdn0cl  13817  crt  13972  phimullem  13973  eulerthlem1  13975  eulerthlem2  13976  pcpremul  14029  prmreclem3  14098  sectcan  14814  sectco  14815  sectmon  14836  monsect  14837  funcf1  14896  funcsect  14902  invfuc  15004  coapm  15059  catciso  15095  posref  15241  psrel  15493  pstr  15501  mhmf  15589  submss  15598  eqger  15851  eqgcpbl  15855  gaorber  15946  orbstafun  15949  cayleyth  16040  dprdgrp  16612  dprdff  16619  dprdffOLD  16625  ablfac1a  16693  ablfac1b  16694  lmodvscl  17089  lbsss  17282  2idlcpbl  17440  assalmod  17515  mpfind  17747  mdetunilem2  18552  mdetunilem5  18555  mdetunilem6  18556  cnptop1  18979  lmfpm  19032  lmff  19038  lmcnp  19041  flimtop  19671  tlmtmd  19894  ustssxp  19912  ustdiag  19916  ustfilxp  19920  ustbas2  19933  tusbas  19976  imasdsf1olem  20081  xmeter  20141  tmsbas  20191  metustexhalfOLD  20271  metustexhalf  20272  nlmngp  20391  qdensere  20482  blcvx  20508  tgqioo  20510  icccmplem2  20533  reconnlem1  20536  cnmpt2pc  20633  icoopnst  20644  iocopnst  20645  iccpnfcnv  20649  phtpcer  20700  phtpcco2  20704  pcohtpylem  20724  pcohtpy  20725  pcopt  20727  pcopt2  20728  pcorevlem  20731  pcorev2  20733  pcophtb  20734  om1addcl  20738  pi1cpbl  20749  pi1grplem  20754  pi1inv  20757  pi1xfrf  20758  pi1xfr  20760  pi1xfrcnvlem  20761  pi1xfrcnv  20762  pi1cof  20764  pi1coghm  20766  cphphl  20823  cphreccllem  20830  cphsqrcl2  20838  tchclm  20880  tchcph  20885  lmcau  20956  bcthlem4  20971  minveclem4c  21045  minveclem2  21046  minveclem3b  21048  minveclem4  21052  minveclem6  21054  ivthicc  21075  ovolfsval  21087  ovollb2lem  21104  ovolshftlem1  21125  ovolscalem1  21129  ovolicc2lem2  21134  ovolicc2lem5  21137  ovolicopnf  21140  ioombl1lem1  21173  ioombl1lem3  21175  ioombl1lem4  21176  uniioovol  21193  uniioombllem2a  21196  uniioombllem2  21197  uniioombllem3a  21198  uniioombllem3  21199  uniioombllem4  21200  uniioombllem6  21202  vitalilem2  21223  vitalilem3  21224  vitalilem4  21225  i1ff  21288  itg2monolem1  21362  itgreval  21408  ibladd  21432  iblabslem  21439  itgspliticc  21448  itgsplitioo  21449  ditgcl  21467  ditgswap  21468  ditgsplitlem  21469  ditgsplit  21470  limcresi  21494  dvlip2  21601  dveq0  21606  dvcnvre  21625  dvfsumlem2  21633  ftc1a  21643  ply1rem  21769  facth1  21770  fta1glem1  21771  fta1glem2  21772  ig1pcl  21781  ig1pdvds  21782  plyrem  21905  facth  21906  vieta1lem1  21910  vieta1lem2  21911  aaliou3lem3  21944  aaliou3lem7  21949  pserulm  22021  psercnlem2  22023  psercn  22025  pserdvlem1  22026  pserdvlem2  22027  pserdv  22028  abelth2  22041  coseq00topi  22098  coseq0negpitopi  22099  cosordlem  22121  efif1olem1  22132  dvloglem  22227  loglesqr  22330  quart1  22385  quartlem2  22387  quartlem3  22388  quartlem4  22389  quart  22390  asinsinlem  22420  atanlogsublem  22444  atans2  22460  dvatan  22464  rlimcnp2  22494  divsqrsumlem  22507  ftalem5  22548  ftalem7  22550  basellem4  22555  basellem5  22556  perfectlem2  22703  dchrinv  22734  chpdifbndlem1  22936  pntibndlem2  22974  pntlema  22979  pntlemb  22980  pntlemg  22981  pntlemh  22982  pntlemn  22983  pntlemq  22984  pntlemr  22985  pntlemj  22986  pntlemf  22988  pntlemk  22989  pntlemo  22990  pntlemp  22993  pntleml  22994  abvcxp  22998  axtgbtwnid  23061  cgr3simp1  23109  eupacl  23743  grpofo  23839  vcablo  24088  nvvc  24146  sspba  24278  sspg  24279  minvecolem2  24429  minvecolem4c  24433  minvecolem4  24434  minvecolem5  24435  minvecolem6  24436  eleigveccl  25516  xrofsup  26207  eliccelico  26213  elicoelioo  26214  ogrpaddlt  26327  slmdvscl  26376  slmdvsass  26379  rnlogbval  26605  rnlogbcl  26606  nnlogbexp  26609  logbrec  26610  baselsiga  26704  insiga  26726  measfrge0  26763  sibfmbl  26866  eulerpartlemt  26899  eulerpartlemmf  26903  probfinmeasbOLD  26956  tg5segofs  27142  subfacp1lem2a  27213  subfacp1lem2b  27214  subfacp1lem3  27215  subfacp1lem4  27216  subfacp1lem5  27217  sconpht2  27272  sconpi1  27273  cvxscon  27277  cvmlift2lem3  27339  cvmlift2lem5  27341  cvmlift2lem6  27342  cvmlift2lem7  27343  cvmlift2lem12  27348  cvmliftphtlem  27351  cvmliftpht  27352  cvmlift3lem2  27354  cvmlift3lem4  27356  cvmlift3lem5  27357  cvmlift3lem6  27358  ghomgrplem  27453  iblabsnclem  28604  dvasin  28629  isbnd3  28832  heiborlem3  28861  iccbnd  28888  rngohomf  28921  idlss  28965  stoweidlem30  29974  stoweidlem31  29975  stoweidlem38  29982  stoweidlem44  29988  sigardiv  30046  sigarcol  30049  sharhght  30050  sigaradd  30051  cevathlem1  30052  cevathlem2  30053  cevath  30054  lelttrdi  30327  wwlksubclwwlk  30615  clwwnisshclwwn  30622  rusisusgra  30697  chfacfisfcpmat  31342  lshplss  32965  opoccl  33178  opococ  33179  oplecon3  33183  hloml  33341  lclkrslem1  35521  lclkrslem2  35522
  Copyright terms: Public domain W3C validator