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

Theorem simp1d 967
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 955 . 2  |-  ( ( ps  /\  ch  /\  th )  ->  ps )
31, 2syl 15 1  |-  ( ph  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 934
This theorem is referenced by:  simp1bi  970  oeeui  6600  oeeu  6601  erinxp  6733  domssex2  7021  domssex  7022  cantnflem1a  7387  cantnflem1b  7388  cantnflem1c  7389  cantnflem1d  7390  cantnflem1  7391  cantnflem3  7393  cantnflem4  7394  fpwwe2lem7  8258  canthnumlem  8270  canthp1lem2  8275  wuntr  8327  supmul1  9719  supmullem1  9720  supmullem2  9721  supmul  9722  ixxdisj  10671  ixxun  10672  ixxss1  10674  ixxss2  10675  ixxss12  10676  ixxub  10677  ixxlb  10678  iccss2  10720  iocssre  10729  icossre  10730  iccssre  10731  icodisj  10761  iccf1o  10778  xov1plusxeqvd  10780  fzen  10811  intfracq  10963  fldiv  10964  remul  11614  sqrlem6  11733  resqrth  11741  sqrth  11848  ruclem6  12513  ruclem9  12516  ruclem12  12519  gcdn0cl  12693  crt  12846  phimullem  12847  eulerthlem1  12849  eulerthlem2  12850  pcpremul  12896  prmreclem3  12965  sectcan  13658  sectco  13659  sectmon  13680  monsect  13681  funcf1  13740  funcsect  13746  invfuc  13848  coapm  13903  catciso  13939  posref  14085  psrel  14312  pstr  14320  mhmf  14420  submss  14427  eqger  14667  eqgcpbl  14671  gaorber  14762  orbstafun  14765  cayleyth  14790  dprdgrp  15240  dprdff  15247  ablfac1a  15304  ablfac1b  15305  lmodvscl  15644  lbsss  15830  2idlcpbl  15986  assalmod  16060  cnptop1  16972  lmfpm  17023  lmff  17029  lmcnp  17032  flimtop  17660  tlmtmd  17869  imasdsf1olem  17937  xmeter  17979  tmsbas  18029  nlmngp  18188  qdensere  18279  blcvx  18304  tgqioo  18306  icccmplem2  18328  reconnlem1  18331  cnmpt2pc  18426  icoopnst  18437  iocopnst  18438  iccpnfcnv  18442  phtpcer  18493  phtpcco2  18497  pcohtpylem  18517  pcohtpy  18518  pcopt  18520  pcopt2  18521  pcorevlem  18524  pcorev2  18526  pcophtb  18527  om1addcl  18531  pi1cpbl  18542  pi1grplem  18547  pi1inv  18550  pi1xfrf  18551  pi1xfr  18553  pi1xfrcnvlem  18554  pi1xfrcnv  18555  pi1cof  18557  pi1coghm  18559  cphphl  18607  cphreccllem  18614  cphsqrcl2  18622  tchclm  18662  tchcph  18667  lmcau  18738  bcthlem4  18749  minveclem4c  18789  minveclem2  18790  minveclem3b  18792  minveclem4  18796  minveclem6  18798  ivthicc  18818  ovolfsval  18830  ovollb2lem  18847  ovolshftlem1  18868  ovolscalem1  18872  ovolicc2lem2  18877  ovolicc2lem5  18880  ovolicopnf  18883  ioombl1lem1  18915  ioombl1lem3  18917  ioombl1lem4  18918  uniioovol  18934  uniioombllem2a  18937  uniioombllem2  18938  uniioombllem3a  18939  uniioombllem3  18940  uniioombllem4  18941  uniioombllem6  18943  vitalilem2  18964  vitalilem3  18965  vitalilem4  18966  i1ff  19031  itg2monolem1  19105  itgreval  19151  ibladd  19175  iblabslem  19182  itgspliticc  19191  itgsplitioo  19192  ditgcl  19208  ditgswap  19209  ditgsplitlem  19210  ditgsplit  19211  limcresi  19235  dvlip2  19342  dveq0  19347  dvcnvre  19366  dvfsumlem2  19374  ftc1a  19384  mpfind  19428  ply1rem  19549  facth1  19550  fta1glem1  19551  fta1glem2  19552  ig1pcl  19561  ig1pdvds  19562  plyrem  19685  facth  19686  vieta1lem1  19690  vieta1lem2  19691  aaliou3lem3  19724  aaliou3lem7  19729  pserulm  19798  psercnlem2  19800  psercn  19802  pserdvlem1  19803  pserdvlem2  19804  pserdv  19805  abelth2  19818  coseq00topi  19870  coseq0negpitopi  19871  cosordlem  19893  efif1olem1  19904  dvloglem  19995  loglesqr  20098  quart1  20152  quartlem2  20154  quartlem3  20155  quartlem4  20156  quart  20157  asinsinlem  20187  atanlogsublem  20211  atans2  20227  dvatan  20231  rlimcnp2  20261  divsqrsumlem  20274  ftalem5  20314  ftalem7  20316  basellem4  20321  basellem5  20322  perfectlem2  20469  dchrinv  20500  chpdifbndlem1  20702  pntibndlem2  20740  pntlema  20745  pntlemb  20746  pntlemg  20747  pntlemh  20748  pntlemn  20749  pntlemq  20750  pntlemr  20751  pntlemj  20752  pntlemf  20754  pntlemk  20755  pntlemo  20756  pntlemp  20759  pntleml  20760  abvcxp  20764  grpofo  20866  vcablo  21113  nvvc  21171  sspba  21303  sspg  21304  minvecolem2  21454  minvecolem4c  21458  minvecolem4  21459  minvecolem5  21460  minvecolem6  21461  eleigveccl  22539  xrofsup  23255  eliccelico  23270  elicoelioo  23271  xrge0iifhom  23319  rnlogbval  23402  rnlogbcl  23403  nnlogbexp  23406  logbrec  23407  baselsiga  23476  insiga  23498  measfrge0  23533  prob01  23616  probfinmeasbOLD  23631  subfacp1lem2a  23711  subfacp1lem2b  23712  subfacp1lem3  23713  subfacp1lem4  23714  subfacp1lem5  23715  sconpht2  23769  sconpi1  23770  cvxscon  23774  cvmlift2lem3  23836  cvmlift2lem5  23838  cvmlift2lem6  23839  cvmlift2lem7  23840  cvmlift2lem12  23845  cvmliftphtlem  23848  cvmliftpht  23849  cvmlift3lem2  23851  cvmlift3lem4  23853  cvmlift3lem5  23854  cvmlift3lem6  23855  eupacl  23884  ghomgrplem  23996  preorel  25225  fldax1  25428  fldax2  25429  vecax1  25453  icccon3  25701  doma  25728  dedalg  25743  cmpmorp  25779  cmppfc1  25781  dualalg  25782  ehm  25791  vidfunid  25837  isbnd3  26508  heiborlem3  26537  iccbnd  26564  rngohomf  26597  idlss  26641  stoweidlem30  27779  stoweidlem31  27780  stoweidlem38  27787  stoweidlem44  27793  sigardiv  27851  sigarcol  27854  sharhght  27855  sigaradd  27856  cevathlem1  27857  cevathlem2  27858  cevath  27859  lshplss  29171  opoccl  29384  opococ  29385  oplecon3  29389  hloml  29547  lclkrslem1  31727  lclkrslem2  31728
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 177  df-an 360  df-3an 936
  Copyright terms: Public domain W3C validator