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  6183  f1dom3el3dif  6184  f1prex  6197  oeeui  7311  oeeu  7312  erinxp  7445  domssex2  7738  domssex  7739  cantnflem1a  8189  cantnflem1b  8190  cantnflem1c  8191  cantnflem1d  8192  cantnflem1  8193  cantnflem3  8195  cantnflem4  8196  fpwwe2lem7  9060  canthnumlem  9072  canthp1lem2  9077  wuntr  9129  supmul1  10576  supmullem1  10577  supmullem2  10578  supmul  10579  ixxdisj  11650  ixxun  11651  ixxss1  11653  ixxss2  11654  ixxss12  11655  ixxub  11656  ixxlb  11657  ixxlbOLD  11658  iccss2  11705  iocssre  11714  icossre  11715  iccssre  11716  icodisj  11755  iccf1o  11774  xov1plusxeqvd  11776  fzen  11814  intfracq  12083  fldiv  12084  remul  13171  sqrlem6  13290  resqrtth  13298  sqrtth  13406  ruclem6  14265  ruclem9  14268  ruclem12  14271  gcdn0cl  14450  crt  14695  phimullem  14696  eulerthlem1  14698  eulerthlem2  14699  pcpremul  14756  prmreclem3  14825  sectcan  15611  sectco  15612  sectmon  15638  monsect  15639  funcf1  15722  funcsect  15728  invfuc  15830  coapm  15917  catciso  15953  posrefOLD  16148  psrel  16400  pstr  16408  mhmf  16538  submss  16548  eqger  16818  eqgcpbl  16822  gaorber  16913  orbstafun  16916  cayleyth  17007  dprdgrp  17572  dprdff  17580  ablfac1a  17637  ablfac1b  17638  lmodvscl  18043  lbsss  18235  2idlcpbl  18393  assalmod  18478  mpfind  18694  mdetunilem2  19569  mdetunilem5  19572  mdetunilem6  19573  chfacfisfcpmat  19810  cnptop1  20189  lmfpm  20242  lmff  20248  lmcnp  20251  flimtop  20911  tlmtmd  21132  ustssxp  21150  ustdiag  21154  ustfilxp  21158  ustbas2  21171  tusbas  21214  imasdsf1olem  21319  xmeter  21379  tmsbas  21429  metustexhalf  21502  nlmngp  21611  qdensere  21701  blcvx  21727  tgqioo  21729  icccmplem2  21752  reconnlem1  21755  cnmpt2pc  21852  icoopnst  21863  iocopnst  21864  iccpnfcnv  21868  phtpcer  21919  phtpcco2  21923  pcohtpylem  21943  pcohtpy  21944  pcopt  21946  pcopt2  21947  pcorevlem  21950  pcorev2  21952  pcophtb  21953  om1addcl  21957  pi1cpbl  21968  pi1grplem  21973  pi1inv  21976  pi1xfrf  21977  pi1xfr  21979  pi1xfrcnvlem  21980  pi1xfrcnv  21981  pi1cof  21983  pi1coghm  21985  cphphl  22042  cphreccllem  22049  cphsqrtcl2  22057  tchclm  22099  tchcph  22104  lmcau  22175  bcthlem4  22188  minveclem4c  22260  minveclem2  22261  minveclem3b  22263  minveclem4  22267  minveclem6  22269  ivthicc  22290  ovolfsval  22302  ovollb2lem  22319  ovolshftlem1  22340  ovolscalem1  22344  ovolicc2lem2  22349  ovolicc2lem5  22352  ovolicopnf  22355  ioombl1lem1  22388  ioombl1lem3  22390  ioombl1lem4  22391  uniioovol  22413  uniioombllem2a  22416  uniioombllem2  22417  uniioombllem2OLD  22418  uniioombllem3a  22419  uniioombllem3  22420  uniioombllem4  22421  uniioombllem6  22423  vitalilem2  22444  vitalilem3  22445  vitalilem4  22446  i1ff  22511  itg2monolem1  22585  itgreval  22631  ibladd  22655  iblabslem  22662  itgspliticc  22671  itgsplitioo  22672  ditgcl  22690  ditgswap  22691  ditgsplitlem  22692  ditgsplit  22693  limcresi  22717  dvlip2  22824  dveq0  22829  dvcnvre  22848  dvfsumlem2  22856  ftc1a  22866  ply1rem  22989  facth1  22990  fta1glem1  22991  fta1glem2  22992  ig1pcl  23001  ig1pdvds  23002  plyrem  23126  facth  23127  vieta1lem1  23131  vieta1lem2  23132  aaliou3lem3  23165  aaliou3lem7  23170  pserulm  23242  psercnlem2  23244  psercn  23246  pserdvlem1  23247  pserdvlem2  23248  pserdv  23249  abelth2  23262  coseq00topi  23322  coseq0negpitopi  23323  cosordlem  23345  efif1olem1  23356  dvloglem  23458  loglesqrt  23563  relogbval  23574  nnlogbexp  23583  logbrec  23584  quart1  23647  quartlem2  23649  quartlem3  23650  quartlem4  23651  quart  23652  asinsinlem  23682  atanlogsublem  23706  atans2  23722  dvatan  23726  rlimcnp2  23757  divsqrtsumlem  23770  ftalem5  23866  ftalem7  23868  basellem4  23873  basellem5  23874  perfectlem2  24021  dchrinv  24052  chpdifbndlem1  24254  pntibndlem2  24292  pntlema  24297  pntlemb  24298  pntlemg  24299  pntlemh  24300  pntlemn  24301  pntlemq  24302  pntlemr  24303  pntlemj  24304  pntlemf  24306  pntlemk  24307  pntlemo  24308  pntlemp  24311  pntleml  24312  abvcxp  24316  axtgbtwnid  24377  cgr3simp1  24427  hlne1  24510  hltr  24515  btwnhl  24519  mirhl  24583  opphllem4  24649  inagswap  24733  wwlksubclwwlk  25377  clwwnisshclwwn  25382  rusisusgra  25504  eupacl  25542  grpofo  25772  vcablo  26021  nvvc  26079  sspba  26211  sspg  26212  minvecolem2  26362  minvecolem4c  26366  minvecolem4  26367  minvecolem5  26368  minvecolem6  26369  eleigveccl  27447  xrofsup  28189  eliccelico  28195  elicoelioo  28196  slmdvscl  28368  slmdvsass  28371  baselsiga  28776  insiga  28798  ldsysgenld  28821  sigapildsys  28823  ldgenpisyslem1  28824  measfrge0  28864  sibfmbl  28996  eulerpartlemt  29030  eulerpartlemmf  29034  probfinmeasbOLD  29087  tg5segofs  29278  subfacp1lem2a  29691  subfacp1lem2b  29692  subfacp1lem3  29693  subfacp1lem4  29694  subfacp1lem5  29695  sconpht2  29749  sconpi1  29750  cvxscon  29754  cvmlift2lem3  29816  cvmlift2lem5  29818  cvmlift2lem6  29819  cvmlift2lem7  29820  cvmlift2lem12  29825  cvmliftphtlem  29828  cvmliftpht  29829  cvmlift3lem2  29831  cvmlift3lem4  29833  cvmlift3lem5  29834  cvmlift3lem6  29835  msrf  29968  elmsta  29974  mthmpps  30008  mclsppslem  30009  mclspps  30010  ghomgrplem  30095  iblabsnclem  31709  dvasin  31732  isbnd3  31820  heiborlem3  31849  iccbnd  31876  rngohomf  31909  idlss  31953  lshplss  32256  opoccl  32469  opococ  32470  oplecon3  32474  hloml  32632  lclkrslem1  34814  lclkrslem2  34815  eliccre  37188  eliocre  37194  icoiccdif  37210  limccog  37272  lptioo1  37284  cncfiooicclem1  37343  cncfioobdlem  37346  ditgeqiooicc  37406  stoweidlem30  37460  stoweidlem31  37461  stoweidlem38  37468  stoweidlem44  37474  fourierdlem26  37564  fourierdlem32  37570  fourierdlem33  37571  fourierdlem37  37575  fourierdlem42  37580  fourierdlem54  37592  fourierdlem63  37601  fourierdlem64  37602  fourierdlem65  37603  fourierdlem69  37607  fourierdlem79  37617  fourierdlem82  37620  fourierdlem89  37627  fourierdlem90  37628  fourierdlem91  37629  fourierdlem111  37649  0sal  37728  sigardiv  37870  sigarcol  37873  sharhght  37874  sigaradd  37875  cevathlem1  37876  cevathlem2  37877  cevath  37878  perfectALTVlem2  38234  proththd  38304  lelttrdi  38396
  Copyright terms: Public domain W3C validator