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  5975  f1dom3el3dif  5976  oeeui  7033  oeeu  7034  erinxp  7166  domssex2  7463  domssex  7464  cantnflem1a  7885  cantnflem1b  7886  cantnflem1c  7887  cantnflem1d  7888  cantnflem1  7889  cantnflem3  7891  cantnflem4  7892  cantnflem1aOLD  7908  cantnflem1bOLD  7909  cantnflem1cOLD  7910  cantnflem1dOLD  7911  cantnflem1OLD  7912  cantnflem3OLD  7913  cantnflem4OLD  7914  fpwwe2lem7  8795  canthnumlem  8807  canthp1lem2  8812  wuntr  8864  supmul1  10287  supmullem1  10288  supmullem2  10289  supmul  10290  ixxdisj  11307  ixxun  11308  ixxss1  11310  ixxss2  11311  ixxss12  11312  ixxub  11313  ixxlb  11314  iccss2  11358  iocssre  11367  icossre  11368  iccssre  11369  icodisj  11402  iccf1o  11421  xov1plusxeqvd  11423  fzen  11459  intfracq  11690  fldiv  11691  remul  12610  sqrlem6  12729  resqrth  12737  sqrth  12844  ruclem6  13509  ruclem9  13512  ruclem12  13515  gcdn0cl  13690  crt  13845  phimullem  13846  eulerthlem1  13848  eulerthlem2  13849  pcpremul  13902  prmreclem3  13971  sectcan  14686  sectco  14687  sectmon  14708  monsect  14709  funcf1  14768  funcsect  14774  invfuc  14876  coapm  14931  catciso  14967  posref  15113  psrel  15365  pstr  15373  mhmf  15461  submss  15469  eqger  15722  eqgcpbl  15726  gaorber  15817  orbstafun  15820  cayleyth  15911  dprdgrp  16477  dprdff  16484  dprdffOLD  16490  ablfac1a  16558  ablfac1b  16559  lmodvscl  16943  lbsss  17135  2idlcpbl  17293  assalmod  17368  mpfind  17597  mdetunilem2  18394  mdetunilem5  18397  mdetunilem6  18398  cnptop1  18821  lmfpm  18874  lmff  18880  lmcnp  18883  flimtop  19513  tlmtmd  19736  ustssxp  19754  ustdiag  19758  ustfilxp  19762  ustbas2  19775  tusbas  19818  imasdsf1olem  19923  xmeter  19983  tmsbas  20033  metustexhalfOLD  20113  metustexhalf  20114  nlmngp  20233  qdensere  20324  blcvx  20350  tgqioo  20352  icccmplem2  20375  reconnlem1  20378  cnmpt2pc  20475  icoopnst  20486  iocopnst  20487  iccpnfcnv  20491  phtpcer  20542  phtpcco2  20546  pcohtpylem  20566  pcohtpy  20567  pcopt  20569  pcopt2  20570  pcorevlem  20573  pcorev2  20575  pcophtb  20576  om1addcl  20580  pi1cpbl  20591  pi1grplem  20596  pi1inv  20599  pi1xfrf  20600  pi1xfr  20602  pi1xfrcnvlem  20603  pi1xfrcnv  20604  pi1cof  20606  pi1coghm  20608  cphphl  20665  cphreccllem  20672  cphsqrcl2  20680  tchclm  20722  tchcph  20727  lmcau  20798  bcthlem4  20813  minveclem4c  20887  minveclem2  20888  minveclem3b  20890  minveclem4  20894  minveclem6  20896  ivthicc  20917  ovolfsval  20929  ovollb2lem  20946  ovolshftlem1  20967  ovolscalem1  20971  ovolicc2lem2  20976  ovolicc2lem5  20979  ovolicopnf  20982  ioombl1lem1  21014  ioombl1lem3  21016  ioombl1lem4  21017  uniioovol  21034  uniioombllem2a  21037  uniioombllem2  21038  uniioombllem3a  21039  uniioombllem3  21040  uniioombllem4  21041  uniioombllem6  21043  vitalilem2  21064  vitalilem3  21065  vitalilem4  21066  i1ff  21129  itg2monolem1  21203  itgreval  21249  ibladd  21273  iblabslem  21280  itgspliticc  21289  itgsplitioo  21290  ditgcl  21308  ditgswap  21309  ditgsplitlem  21310  ditgsplit  21311  limcresi  21335  dvlip2  21442  dveq0  21447  dvcnvre  21466  dvfsumlem2  21474  ftc1a  21484  ply1rem  21610  facth1  21611  fta1glem1  21612  fta1glem2  21613  ig1pcl  21622  ig1pdvds  21623  plyrem  21746  facth  21747  vieta1lem1  21751  vieta1lem2  21752  aaliou3lem3  21785  aaliou3lem7  21790  pserulm  21862  psercnlem2  21864  psercn  21866  pserdvlem1  21867  pserdvlem2  21868  pserdv  21869  abelth2  21882  coseq00topi  21939  coseq0negpitopi  21940  cosordlem  21962  efif1olem1  21973  dvloglem  22068  loglesqr  22171  quart1  22226  quartlem2  22228  quartlem3  22229  quartlem4  22230  quart  22231  asinsinlem  22261  atanlogsublem  22285  atans2  22301  dvatan  22305  rlimcnp2  22335  divsqrsumlem  22348  ftalem5  22389  ftalem7  22391  basellem4  22396  basellem5  22397  perfectlem2  22544  dchrinv  22575  chpdifbndlem1  22777  pntibndlem2  22815  pntlema  22820  pntlemb  22821  pntlemg  22822  pntlemh  22823  pntlemn  22824  pntlemq  22825  pntlemr  22826  pntlemj  22827  pntlemf  22829  pntlemk  22830  pntlemo  22831  pntlemp  22834  pntleml  22835  abvcxp  22839  axtgbtwnid  22902  cgr3simp1  22947  eupacl  23541  grpofo  23637  vcablo  23886  nvvc  23944  sspba  24076  sspg  24077  minvecolem2  24227  minvecolem4c  24231  minvecolem4  24232  minvecolem5  24233  minvecolem6  24234  eleigveccl  25314  xrofsup  26006  eliccelico  26018  elicoelioo  26019  ogrpaddlt  26132  slmdvscl  26181  slmdvsass  26184  rnlogbval  26411  rnlogbcl  26412  nnlogbexp  26415  logbrec  26416  baselsiga  26510  insiga  26532  measfrge0  26569  sibfmbl  26673  eulerpartlemt  26706  eulerpartlemmf  26710  probfinmeasbOLD  26763  tg5segofs  26949  subfacp1lem2a  27020  subfacp1lem2b  27021  subfacp1lem3  27022  subfacp1lem4  27023  subfacp1lem5  27024  sconpht2  27079  sconpi1  27080  cvxscon  27084  cvmlift2lem3  27146  cvmlift2lem5  27148  cvmlift2lem6  27149  cvmlift2lem7  27150  cvmlift2lem12  27155  cvmliftphtlem  27158  cvmliftpht  27159  cvmlift3lem2  27161  cvmlift3lem4  27163  cvmlift3lem5  27164  cvmlift3lem6  27165  ghomgrplem  27259  iblabsnclem  28408  dvasin  28433  isbnd3  28636  heiborlem3  28665  iccbnd  28692  rngohomf  28725  idlss  28769  stoweidlem30  29778  stoweidlem31  29779  stoweidlem38  29786  stoweidlem44  29792  sigardiv  29850  sigarcol  29853  sharhght  29854  sigaradd  29855  cevathlem1  29856  cevathlem2  29857  cevath  29858  lelttrdi  30131  wwlksubclwwlk  30419  clwwnisshclwwn  30426  rusisusgra  30501  lshplss  32466  opoccl  32679  opococ  32680  oplecon3  32684  hloml  32842  lclkrslem1  35022  lclkrslem2  35023
  Copyright terms: Public domain W3C validator