MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  simp1d 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  6804  oeeu  6805  erinxp  6937  domssex2  7226  domssex  7227  cantnflem1a  7597  cantnflem1b  7598  cantnflem1c  7599  cantnflem1d  7600  cantnflem1  7601  cantnflem3  7603  cantnflem4  7604  fpwwe2lem7  8467  canthnumlem  8479  canthp1lem2  8484  wuntr  8536  supmul1  9929  supmullem1  9930  supmullem2  9931  supmul  9932  ixxdisj  10887  ixxun  10888  ixxss1  10890  ixxss2  10891  ixxss12  10892  ixxub  10893  ixxlb  10894  iccss2  10937  iocssre  10946  icossre  10947  iccssre  10948  icodisj  10978  iccf1o  10995  xov1plusxeqvd  10997  fzen  11028  intfracq  11195  fldiv  11196  remul  11889  sqrlem6  12008  resqrth  12016  sqrth  12123  ruclem6  12789  ruclem9  12792  ruclem12  12795  gcdn0cl  12969  crt  13122  phimullem  13123  eulerthlem1  13125  eulerthlem2  13126  pcpremul  13172  prmreclem3  13241  sectcan  13936  sectco  13937  sectmon  13958  monsect  13959  funcf1  14018  funcsect  14024  invfuc  14126  coapm  14181  catciso  14217  posref  14363  psrel  14590  pstr  14598  mhmf  14698  submss  14705  eqger  14945  eqgcpbl  14949  gaorber  15040  orbstafun  15043  cayleyth  15068  dprdgrp  15518  dprdff  15525  ablfac1a  15582  ablfac1b  15583  lmodvscl  15922  lbsss  16104  2idlcpbl  16260  assalmod  16334  cnptop1  17260  lmfpm  17313  lmff  17319  lmcnp  17322  flimtop  17950  tlmtmd  18169  ustssxp  18187  ustdiag  18191  ustfilxp  18195  ustbas2  18208  tusbas  18251  imasdsf1olem  18356  xmeter  18416  tmsbas  18466  metustexhalfOLD  18546  metustexhalf  18547  nlmngp  18666  qdensere  18757  blcvx  18782  tgqioo  18784  icccmplem2  18807  reconnlem1  18810  cnmpt2pc  18906  icoopnst  18917  iocopnst  18918  iccpnfcnv  18922  phtpcer  18973  phtpcco2  18977  pcohtpylem  18997  pcohtpy  18998  pcopt  19000  pcopt2  19001  pcorevlem  19004  pcorev2  19006  pcophtb  19007  om1addcl  19011  pi1cpbl  19022  pi1grplem  19027  pi1inv  19030  pi1xfrf  19031  pi1xfr  19033  pi1xfrcnvlem  19034  pi1xfrcnv  19035  pi1cof  19037  pi1coghm  19039  cphphl  19087  cphreccllem  19094  cphsqrcl2  19102  tchclm  19142  tchcph  19147  lmcau  19218  bcthlem4  19233  minveclem4c  19279  minveclem2  19280  minveclem3b  19282  minveclem4  19286  minveclem6  19288  ivthicc  19308  ovolfsval  19320  ovollb2lem  19337  ovolshftlem1  19358  ovolscalem1  19362  ovolicc2lem2  19367  ovolicc2lem5  19370  ovolicopnf  19373  ioombl1lem1  19405  ioombl1lem3  19407  ioombl1lem4  19408  uniioovol  19424  uniioombllem2a  19427  uniioombllem2  19428  uniioombllem3a  19429  uniioombllem3  19430  uniioombllem4  19431  uniioombllem6  19433  vitalilem2  19454  vitalilem3  19455  vitalilem4  19456  i1ff  19521  itg2monolem1  19595  itgreval  19641  ibladd  19665  iblabslem  19672  itgspliticc  19681  itgsplitioo  19682  ditgcl  19698  ditgswap  19699  ditgsplitlem  19700  ditgsplit  19701  limcresi  19725  dvlip2  19832  dveq0  19837  dvcnvre  19856  dvfsumlem2  19864  ftc1a  19874  mpfind  19918  ply1rem  20039  facth1  20040  fta1glem1  20041  fta1glem2  20042  ig1pcl  20051  ig1pdvds  20052  plyrem  20175  facth  20176  vieta1lem1  20180  vieta1lem2  20181  aaliou3lem3  20214  aaliou3lem7  20219  pserulm  20291  psercnlem2  20293  psercn  20295  pserdvlem1  20296  pserdvlem2  20297  pserdv  20298  abelth2  20311  coseq00topi  20363  coseq0negpitopi  20364  cosordlem  20386  efif1olem1  20397  dvloglem  20492  loglesqr  20595  quart1  20649  quartlem2  20651  quartlem3  20652  quartlem4  20653  quart  20654  asinsinlem  20684  atanlogsublem  20708  atans2  20724  dvatan  20728  rlimcnp2  20758  divsqrsumlem  20771  ftalem5  20812  ftalem7  20814  basellem4  20819  basellem5  20820  perfectlem2  20967  dchrinv  20998  chpdifbndlem1  21200  pntibndlem2  21238  pntlema  21243  pntlemb  21244  pntlemg  21245  pntlemh  21246  pntlemn  21247  pntlemq  21248  pntlemr  21249  pntlemj  21250  pntlemf  21252  pntlemk  21253  pntlemo  21254  pntlemp  21257  pntleml  21258  abvcxp  21262  eupacl  21644  grpofo  21740  vcablo  21989  nvvc  22047  sspba  22179  sspg  22180  minvecolem2  22330  minvecolem4c  22334  minvecolem4  22335  minvecolem5  22336  minvecolem6  22337  eleigveccl  23415  xrofsup  24079  eliccelico  24093  elicoelioo  24094  rnlogbval  24353  rnlogbcl  24354  nnlogbexp  24357  logbrec  24358  baselsiga  24451  insiga  24473  measfrge0  24510  sibfmbl  24603  probfinmeasbOLD  24639  subfacp1lem2a  24819  subfacp1lem2b  24820  subfacp1lem3  24821  subfacp1lem4  24822  subfacp1lem5  24823  sconpht2  24878  sconpi1  24879  cvxscon  24883  cvmlift2lem3  24945  cvmlift2lem5  24947  cvmlift2lem6  24948  cvmlift2lem7  24949  cvmlift2lem12  24954  cvmliftphtlem  24957  cvmliftpht  24958  cvmlift3lem2  24960  cvmlift3lem4  24962  cvmlift3lem5  24963  cvmlift3lem6  24964  ghomgrplem  25053  iblabsnclem  26167  isbnd3  26383  heiborlem3  26412  iccbnd  26439  rngohomf  26472  idlss  26516  stoweidlem30  27646  stoweidlem31  27647  stoweidlem38  27654  stoweidlem44  27660  sigardiv  27718  sigarcol  27721  sharhght  27722  sigaradd  27723  cevathlem1  27724  cevathlem2  27725  cevath  27726  lshplss  29464  opoccl  29677  opococ  29678  oplecon3  29682  hloml  29840  lclkrslem1  32020  lclkrslem2  32021
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