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

Theorem simp1d 1008
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 996 . 2  |-  ( ( ps  /\  ch  /\  th )  ->  ps )
31, 2syl 16 1  |-  ( ph  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ w3a 973
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 975
This theorem is referenced by:  simp1bi  1011  f1dom3fv3dif  6161  f1dom3el3dif  6162  oeeui  7248  oeeu  7249  erinxp  7382  domssex2  7674  domssex  7675  cantnflem1a  8100  cantnflem1b  8101  cantnflem1c  8102  cantnflem1d  8103  cantnflem1  8104  cantnflem3  8106  cantnflem4  8107  cantnflem1aOLD  8123  cantnflem1bOLD  8124  cantnflem1cOLD  8125  cantnflem1dOLD  8126  cantnflem1OLD  8127  cantnflem3OLD  8128  cantnflem4OLD  8129  fpwwe2lem7  9010  canthnumlem  9022  canthp1lem2  9027  wuntr  9079  supmul1  10504  supmullem1  10505  supmullem2  10506  supmul  10507  ixxdisj  11540  ixxun  11541  ixxss1  11543  ixxss2  11544  ixxss12  11545  ixxub  11546  ixxlb  11547  iccss2  11591  iocssre  11600  icossre  11601  iccssre  11602  icodisj  11641  iccf1o  11660  xov1plusxeqvd  11662  fzen  11699  intfracq  11950  fldiv  11951  remul  12921  sqrlem6  13040  resqrtth  13048  sqrtth  13156  ruclem6  13825  ruclem9  13828  ruclem12  13831  gcdn0cl  14007  crt  14163  phimullem  14164  eulerthlem1  14166  eulerthlem2  14167  pcpremul  14222  prmreclem3  14291  sectcan  15007  sectco  15008  sectmon  15029  monsect  15030  funcf1  15089  funcsect  15095  invfuc  15197  coapm  15252  catciso  15288  posref  15434  psrel  15686  pstr  15694  mhmf  15782  submss  15791  eqger  16046  eqgcpbl  16050  gaorber  16141  orbstafun  16144  cayleyth  16235  dprdgrp  16829  dprdff  16836  dprdffOLD  16842  ablfac1a  16910  ablfac1b  16911  lmodvscl  17312  lbsss  17506  2idlcpbl  17664  assalmod  17739  mpfind  17976  mdetunilem2  18882  mdetunilem5  18885  mdetunilem6  18886  chfacfisfcpmat  19123  cnptop1  19509  lmfpm  19562  lmff  19568  lmcnp  19571  flimtop  20201  tlmtmd  20424  ustssxp  20442  ustdiag  20446  ustfilxp  20450  ustbas2  20463  tusbas  20506  imasdsf1olem  20611  xmeter  20671  tmsbas  20721  metustexhalfOLD  20801  metustexhalf  20802  nlmngp  20921  qdensere  21012  blcvx  21038  tgqioo  21040  icccmplem2  21063  reconnlem1  21066  cnmpt2pc  21163  icoopnst  21174  iocopnst  21175  iccpnfcnv  21179  phtpcer  21230  phtpcco2  21234  pcohtpylem  21254  pcohtpy  21255  pcopt  21257  pcopt2  21258  pcorevlem  21261  pcorev2  21263  pcophtb  21264  om1addcl  21268  pi1cpbl  21279  pi1grplem  21284  pi1inv  21287  pi1xfrf  21288  pi1xfr  21290  pi1xfrcnvlem  21291  pi1xfrcnv  21292  pi1cof  21294  pi1coghm  21296  cphphl  21353  cphreccllem  21360  cphsqrtcl2  21368  tchclm  21410  tchcph  21415  lmcau  21486  bcthlem4  21501  minveclem4c  21575  minveclem2  21576  minveclem3b  21578  minveclem4  21582  minveclem6  21584  ivthicc  21605  ovolfsval  21617  ovollb2lem  21634  ovolshftlem1  21655  ovolscalem1  21659  ovolicc2lem2  21664  ovolicc2lem5  21667  ovolicopnf  21670  ioombl1lem1  21703  ioombl1lem3  21705  ioombl1lem4  21706  uniioovol  21723  uniioombllem2a  21726  uniioombllem2  21727  uniioombllem3a  21728  uniioombllem3  21729  uniioombllem4  21730  uniioombllem6  21732  vitalilem2  21753  vitalilem3  21754  vitalilem4  21755  i1ff  21818  itg2monolem1  21892  itgreval  21938  ibladd  21962  iblabslem  21969  itgspliticc  21978  itgsplitioo  21979  ditgcl  21997  ditgswap  21998  ditgsplitlem  21999  ditgsplit  22000  limcresi  22024  dvlip2  22131  dveq0  22136  dvcnvre  22155  dvfsumlem2  22163  ftc1a  22173  ply1rem  22299  facth1  22300  fta1glem1  22301  fta1glem2  22302  ig1pcl  22311  ig1pdvds  22312  plyrem  22435  facth  22436  vieta1lem1  22440  vieta1lem2  22441  aaliou3lem3  22474  aaliou3lem7  22479  pserulm  22551  psercnlem2  22553  psercn  22555  pserdvlem1  22556  pserdvlem2  22557  pserdv  22558  abelth2  22571  coseq00topi  22628  coseq0negpitopi  22629  cosordlem  22651  efif1olem1  22662  dvloglem  22757  loglesqrt  22860  quart1  22915  quartlem2  22917  quartlem3  22918  quartlem4  22919  quart  22920  asinsinlem  22950  atanlogsublem  22974  atans2  22990  dvatan  22994  rlimcnp2  23024  divsqrtsumlem  23037  ftalem5  23078  ftalem7  23080  basellem4  23085  basellem5  23086  perfectlem2  23233  dchrinv  23264  chpdifbndlem1  23466  pntibndlem2  23504  pntlema  23509  pntlemb  23510  pntlemg  23511  pntlemh  23512  pntlemn  23513  pntlemq  23514  pntlemr  23515  pntlemj  23516  pntlemf  23518  pntlemk  23519  pntlemo  23520  pntlemp  23523  pntleml  23524  abvcxp  23528  axtgbtwnid  23591  cgr3simp1  23639  wwlksubclwwlk  24480  clwwnisshclwwn  24485  rusisusgra  24607  eupacl  24645  grpofo  24877  vcablo  25126  nvvc  25184  sspba  25316  sspg  25317  minvecolem2  25467  minvecolem4c  25471  minvecolem4  25472  minvecolem5  25473  minvecolem6  25474  eleigveccl  26554  xrofsup  27250  eliccelico  27256  elicoelioo  27257  ogrpaddlt  27370  slmdvscl  27419  slmdvsass  27422  rnlogbval  27656  rnlogbcl  27657  nnlogbexp  27660  logbrec  27661  baselsiga  27755  insiga  27777  measfrge0  27814  sibfmbl  27917  eulerpartlemt  27950  eulerpartlemmf  27954  probfinmeasbOLD  28007  tg5segofs  28193  subfacp1lem2a  28264  subfacp1lem2b  28265  subfacp1lem3  28266  subfacp1lem4  28267  subfacp1lem5  28268  sconpht2  28323  sconpi1  28324  cvxscon  28328  cvmlift2lem3  28390  cvmlift2lem5  28392  cvmlift2lem6  28393  cvmlift2lem7  28394  cvmlift2lem12  28399  cvmliftphtlem  28402  cvmliftpht  28403  cvmlift3lem2  28405  cvmlift3lem4  28407  cvmlift3lem5  28408  cvmlift3lem6  28409  ghomgrplem  28504  iblabsnclem  29655  dvasin  29680  isbnd3  29883  heiborlem3  29912  iccbnd  29939  rngohomf  29972  idlss  30016  eliccre  31104  eliocre  31111  icoiccdif  31128  limccog  31162  lptioo1  31174  cncfiooicclem1  31232  cncfioobdlem  31235  ditgeqiooicc  31278  stoweidlem30  31330  stoweidlem31  31331  stoweidlem38  31338  stoweidlem44  31344  fourierdlem26  31433  fourierdlem32  31439  fourierdlem33  31440  fourierdlem37  31444  fourierdlem42  31449  fourierdlem54  31461  fourierdlem63  31470  fourierdlem64  31471  fourierdlem65  31472  fourierdlem69  31476  fourierdlem74  31481  fourierdlem75  31482  fourierdlem79  31486  fourierdlem82  31489  fourierdlem89  31496  fourierdlem90  31497  fourierdlem91  31498  fourierdlem93  31500  fourierdlem111  31518  sigardiv  31545  sigarcol  31548  sharhght  31549  sigaradd  31550  cevathlem1  31551  cevathlem2  31552  cevath  31553  lelttrdi  31792  lshplss  33778  opoccl  33991  opococ  33992  oplecon3  33996  hloml  34154  lclkrslem1  36334  lclkrslem2  36335
  Copyright terms: Public domain W3C validator