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

Theorem simp1d 969
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 957 . 2  |-  ( ( ps  /\  ch  /\  th )  ->  ps )
31, 2syl 16 1  |-  ( ph  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 936
This theorem is referenced by:  simp1bi  972  oeeui  6837  oeeu  6838  erinxp  6970  domssex2  7259  domssex  7260  cantnflem1a  7633  cantnflem1b  7634  cantnflem1c  7635  cantnflem1d  7636  cantnflem1  7637  cantnflem3  7639  cantnflem4  7640  fpwwe2lem7  8503  canthnumlem  8515  canthp1lem2  8520  wuntr  8572  supmul1  9965  supmullem1  9966  supmullem2  9967  supmul  9968  ixxdisj  10923  ixxun  10924  ixxss1  10926  ixxss2  10927  ixxss12  10928  ixxub  10929  ixxlb  10930  iccss2  10973  iocssre  10982  icossre  10983  iccssre  10984  icodisj  11014  iccf1o  11031  xov1plusxeqvd  11033  fzen  11064  intfracq  11232  fldiv  11233  remul  11926  sqrlem6  12045  resqrth  12053  sqrth  12160  ruclem6  12826  ruclem9  12829  ruclem12  12832  gcdn0cl  13006  crt  13159  phimullem  13160  eulerthlem1  13162  eulerthlem2  13163  pcpremul  13209  prmreclem3  13278  sectcan  13973  sectco  13974  sectmon  13995  monsect  13996  funcf1  14055  funcsect  14061  invfuc  14163  coapm  14218  catciso  14254  posref  14400  psrel  14627  pstr  14635  mhmf  14735  submss  14742  eqger  14982  eqgcpbl  14986  gaorber  15077  orbstafun  15080  cayleyth  15105  dprdgrp  15555  dprdff  15562  ablfac1a  15619  ablfac1b  15620  lmodvscl  15959  lbsss  16141  2idlcpbl  16297  assalmod  16371  cnptop1  17298  lmfpm  17351  lmff  17357  lmcnp  17360  flimtop  17989  tlmtmd  18208  ustssxp  18226  ustdiag  18230  ustfilxp  18234  ustbas2  18247  tusbas  18290  imasdsf1olem  18395  xmeter  18455  tmsbas  18505  metustexhalfOLD  18585  metustexhalf  18586  nlmngp  18705  qdensere  18796  blcvx  18821  tgqioo  18823  icccmplem2  18846  reconnlem1  18849  cnmpt2pc  18945  icoopnst  18956  iocopnst  18957  iccpnfcnv  18961  phtpcer  19012  phtpcco2  19016  pcohtpylem  19036  pcohtpy  19037  pcopt  19039  pcopt2  19040  pcorevlem  19043  pcorev2  19045  pcophtb  19046  om1addcl  19050  pi1cpbl  19061  pi1grplem  19066  pi1inv  19069  pi1xfrf  19070  pi1xfr  19072  pi1xfrcnvlem  19073  pi1xfrcnv  19074  pi1cof  19076  pi1coghm  19078  cphphl  19126  cphreccllem  19133  cphsqrcl2  19141  tchclm  19181  tchcph  19186  lmcau  19257  bcthlem4  19272  minveclem4c  19318  minveclem2  19319  minveclem3b  19321  minveclem4  19325  minveclem6  19327  ivthicc  19347  ovolfsval  19359  ovollb2lem  19376  ovolshftlem1  19397  ovolscalem1  19401  ovolicc2lem2  19406  ovolicc2lem5  19409  ovolicopnf  19412  ioombl1lem1  19444  ioombl1lem3  19446  ioombl1lem4  19447  uniioovol  19463  uniioombllem2a  19466  uniioombllem2  19467  uniioombllem3a  19468  uniioombllem3  19469  uniioombllem4  19470  uniioombllem6  19472  vitalilem2  19493  vitalilem3  19494  vitalilem4  19495  i1ff  19560  itg2monolem1  19634  itgreval  19680  ibladd  19704  iblabslem  19711  itgspliticc  19720  itgsplitioo  19721  ditgcl  19737  ditgswap  19738  ditgsplitlem  19739  ditgsplit  19740  limcresi  19764  dvlip2  19871  dveq0  19876  dvcnvre  19895  dvfsumlem2  19903  ftc1a  19913  mpfind  19957  ply1rem  20078  facth1  20079  fta1glem1  20080  fta1glem2  20081  ig1pcl  20090  ig1pdvds  20091  plyrem  20214  facth  20215  vieta1lem1  20219  vieta1lem2  20220  aaliou3lem3  20253  aaliou3lem7  20258  pserulm  20330  psercnlem2  20332  psercn  20334  pserdvlem1  20335  pserdvlem2  20336  pserdv  20337  abelth2  20350  coseq00topi  20402  coseq0negpitopi  20403  cosordlem  20425  efif1olem1  20436  dvloglem  20531  loglesqr  20634  quart1  20688  quartlem2  20690  quartlem3  20691  quartlem4  20692  quart  20693  asinsinlem  20723  atanlogsublem  20747  atans2  20763  dvatan  20767  rlimcnp2  20797  divsqrsumlem  20810  ftalem5  20851  ftalem7  20853  basellem4  20858  basellem5  20859  perfectlem2  21006  dchrinv  21037  chpdifbndlem1  21239  pntibndlem2  21277  pntlema  21282  pntlemb  21283  pntlemg  21284  pntlemh  21285  pntlemn  21286  pntlemq  21287  pntlemr  21288  pntlemj  21289  pntlemf  21291  pntlemk  21292  pntlemo  21293  pntlemp  21296  pntleml  21297  abvcxp  21301  eupacl  21683  grpofo  21779  vcablo  22028  nvvc  22086  sspba  22218  sspg  22219  minvecolem2  22369  minvecolem4c  22373  minvecolem4  22374  minvecolem5  22375  minvecolem6  22376  eleigveccl  23454  xrofsup  24118  eliccelico  24132  elicoelioo  24133  rnlogbval  24392  rnlogbcl  24393  nnlogbexp  24396  logbrec  24397  baselsiga  24490  insiga  24512  measfrge0  24549  sibfmbl  24642  probfinmeasbOLD  24678  subfacp1lem2a  24858  subfacp1lem2b  24859  subfacp1lem3  24860  subfacp1lem4  24861  subfacp1lem5  24862  sconpht2  24917  sconpi1  24918  cvxscon  24922  cvmlift2lem3  24984  cvmlift2lem5  24986  cvmlift2lem6  24987  cvmlift2lem7  24988  cvmlift2lem12  24993  cvmliftphtlem  24996  cvmliftpht  24997  cvmlift3lem2  24999  cvmlift3lem4  25001  cvmlift3lem5  25002  cvmlift3lem6  25003  ghomgrplem  25092  iblabsnclem  26258  isbnd3  26484  heiborlem3  26513  iccbnd  26540  rngohomf  26573  idlss  26617  stoweidlem30  27746  stoweidlem31  27747  stoweidlem38  27754  stoweidlem44  27760  sigardiv  27818  sigarcol  27821  sharhght  27822  sigaradd  27823  cevathlem1  27824  cevathlem2  27825  cevath  27826  lshplss  29716  opoccl  29929  opococ  29930  oplecon3  29934  hloml  30092  lclkrslem1  32272  lclkrslem2  32273
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-an 361  df-3an 938
  Copyright terms: Public domain W3C validator