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  6781  oeeu  6782  erinxp  6914  domssex2  7203  domssex  7204  cantnflem1a  7574  cantnflem1b  7575  cantnflem1c  7576  cantnflem1d  7577  cantnflem1  7578  cantnflem3  7580  cantnflem4  7581  fpwwe2lem7  8444  canthnumlem  8456  canthp1lem2  8461  wuntr  8513  supmul1  9905  supmullem1  9906  supmullem2  9907  supmul  9908  ixxdisj  10863  ixxun  10864  ixxss1  10866  ixxss2  10867  ixxss12  10868  ixxub  10869  ixxlb  10870  iccss2  10913  iocssre  10922  icossre  10923  iccssre  10924  icodisj  10954  iccf1o  10971  xov1plusxeqvd  10973  fzen  11004  intfracq  11167  fldiv  11168  remul  11861  sqrlem6  11980  resqrth  11988  sqrth  12095  ruclem6  12761  ruclem9  12764  ruclem12  12767  gcdn0cl  12941  crt  13094  phimullem  13095  eulerthlem1  13097  eulerthlem2  13098  pcpremul  13144  prmreclem3  13213  sectcan  13908  sectco  13909  sectmon  13930  monsect  13931  funcf1  13990  funcsect  13996  invfuc  14098  coapm  14153  catciso  14189  posref  14335  psrel  14562  pstr  14570  mhmf  14670  submss  14677  eqger  14917  eqgcpbl  14921  gaorber  15012  orbstafun  15015  cayleyth  15040  dprdgrp  15490  dprdff  15497  ablfac1a  15554  ablfac1b  15555  lmodvscl  15894  lbsss  16076  2idlcpbl  16232  assalmod  16306  cnptop1  17228  lmfpm  17281  lmff  17287  lmcnp  17290  flimtop  17918  tlmtmd  18137  ustssxp  18155  ustdiag  18159  ustfilxp  18163  ustbas2  18176  tusbas  18219  imasdsf1olem  18311  xmeter  18353  tmsbas  18403  metustexhalf  18476  nlmngp  18584  qdensere  18675  blcvx  18700  tgqioo  18702  icccmplem2  18725  reconnlem1  18728  cnmpt2pc  18824  icoopnst  18835  iocopnst  18836  iccpnfcnv  18840  phtpcer  18891  phtpcco2  18895  pcohtpylem  18915  pcohtpy  18916  pcopt  18918  pcopt2  18919  pcorevlem  18922  pcorev2  18924  pcophtb  18925  om1addcl  18929  pi1cpbl  18940  pi1grplem  18945  pi1inv  18948  pi1xfrf  18949  pi1xfr  18951  pi1xfrcnvlem  18952  pi1xfrcnv  18953  pi1cof  18955  pi1coghm  18957  cphphl  19005  cphreccllem  19012  cphsqrcl2  19020  tchclm  19060  tchcph  19065  lmcau  19136  bcthlem4  19149  minveclem4c  19193  minveclem2  19194  minveclem3b  19196  minveclem4  19200  minveclem6  19202  ivthicc  19222  ovolfsval  19234  ovollb2lem  19251  ovolshftlem1  19272  ovolscalem1  19276  ovolicc2lem2  19281  ovolicc2lem5  19284  ovolicopnf  19287  ioombl1lem1  19319  ioombl1lem3  19321  ioombl1lem4  19322  uniioovol  19338  uniioombllem2a  19341  uniioombllem2  19342  uniioombllem3a  19343  uniioombllem3  19344  uniioombllem4  19345  uniioombllem6  19347  vitalilem2  19368  vitalilem3  19369  vitalilem4  19370  i1ff  19435  itg2monolem1  19509  itgreval  19555  ibladd  19579  iblabslem  19586  itgspliticc  19595  itgsplitioo  19596  ditgcl  19612  ditgswap  19613  ditgsplitlem  19614  ditgsplit  19615  limcresi  19639  dvlip2  19746  dveq0  19751  dvcnvre  19770  dvfsumlem2  19778  ftc1a  19788  mpfind  19832  ply1rem  19953  facth1  19954  fta1glem1  19955  fta1glem2  19956  ig1pcl  19965  ig1pdvds  19966  plyrem  20089  facth  20090  vieta1lem1  20094  vieta1lem2  20095  aaliou3lem3  20128  aaliou3lem7  20133  pserulm  20205  psercnlem2  20207  psercn  20209  pserdvlem1  20210  pserdvlem2  20211  pserdv  20212  abelth2  20225  coseq00topi  20277  coseq0negpitopi  20278  cosordlem  20300  efif1olem1  20311  dvloglem  20406  loglesqr  20509  quart1  20563  quartlem2  20565  quartlem3  20566  quartlem4  20567  quart  20568  asinsinlem  20598  atanlogsublem  20622  atans2  20638  dvatan  20642  rlimcnp2  20672  divsqrsumlem  20685  ftalem5  20726  ftalem7  20728  basellem4  20733  basellem5  20734  perfectlem2  20881  dchrinv  20912  chpdifbndlem1  21114  pntibndlem2  21152  pntlema  21157  pntlemb  21158  pntlemg  21159  pntlemh  21160  pntlemn  21161  pntlemq  21162  pntlemr  21163  pntlemj  21164  pntlemf  21166  pntlemk  21167  pntlemo  21168  pntlemp  21171  pntleml  21172  abvcxp  21176  eupacl  21539  grpofo  21635  vcablo  21884  nvvc  21942  sspba  22074  sspg  22075  minvecolem2  22225  minvecolem4c  22229  minvecolem4  22230  minvecolem5  22231  minvecolem6  22232  eleigveccl  23310  xrofsup  23962  eliccelico  23976  elicoelioo  23977  rnlogbval  24196  rnlogbcl  24197  nnlogbexp  24200  logbrec  24201  baselsiga  24294  insiga  24316  measfrge0  24352  probfinmeasbOLD  24465  subfacp1lem2a  24645  subfacp1lem2b  24646  subfacp1lem3  24647  subfacp1lem4  24648  subfacp1lem5  24649  sconpht2  24704  sconpi1  24705  cvxscon  24709  cvmlift2lem3  24771  cvmlift2lem5  24773  cvmlift2lem6  24774  cvmlift2lem7  24775  cvmlift2lem12  24780  cvmliftphtlem  24783  cvmliftpht  24784  cvmlift3lem2  24786  cvmlift3lem4  24788  cvmlift3lem5  24789  cvmlift3lem6  24790  ghomgrplem  24879  iblabsnclem  25968  isbnd3  26184  heiborlem3  26213  iccbnd  26240  rngohomf  26273  idlss  26317  stoweidlem30  27447  stoweidlem31  27448  stoweidlem38  27455  stoweidlem44  27461  sigardiv  27519  sigarcol  27522  sharhght  27523  sigaradd  27524  cevathlem1  27525  cevathlem2  27526  cevath  27527  lshplss  29096  opoccl  29309  opococ  29310  oplecon3  29314  hloml  29472  lclkrslem1  31652  lclkrslem2  31653
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