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  6616  oeeu  6617  erinxp  6749  domssex2  7037  domssex  7038  cantnflem1a  7403  cantnflem1b  7404  cantnflem1c  7405  cantnflem1d  7406  cantnflem1  7407  cantnflem3  7409  cantnflem4  7410  fpwwe2lem7  8274  canthnumlem  8286  canthp1lem2  8291  wuntr  8343  supmul1  9735  supmullem1  9736  supmullem2  9737  supmul  9738  ixxdisj  10687  ixxun  10688  ixxss1  10690  ixxss2  10691  ixxss12  10692  ixxub  10693  ixxlb  10694  iccss2  10736  iocssre  10745  icossre  10746  iccssre  10747  icodisj  10777  iccf1o  10794  xov1plusxeqvd  10796  fzen  10827  intfracq  10979  fldiv  10980  remul  11630  sqrlem6  11749  resqrth  11757  sqrth  11864  ruclem6  12529  ruclem9  12532  ruclem12  12535  gcdn0cl  12709  crt  12862  phimullem  12863  eulerthlem1  12865  eulerthlem2  12866  pcpremul  12912  prmreclem3  12981  sectcan  13674  sectco  13675  sectmon  13696  monsect  13697  funcf1  13756  funcsect  13762  invfuc  13864  coapm  13919  catciso  13955  posref  14101  psrel  14328  pstr  14336  mhmf  14436  submss  14443  eqger  14683  eqgcpbl  14687  gaorber  14778  orbstafun  14781  cayleyth  14806  dprdgrp  15256  dprdff  15263  ablfac1a  15320  ablfac1b  15321  lmodvscl  15660  lbsss  15846  2idlcpbl  16002  assalmod  16076  cnptop1  16988  lmfpm  17039  lmff  17045  lmcnp  17048  flimtop  17676  tlmtmd  17885  imasdsf1olem  17953  xmeter  17995  tmsbas  18045  nlmngp  18204  qdensere  18295  blcvx  18320  tgqioo  18322  icccmplem2  18344  reconnlem1  18347  cnmpt2pc  18442  icoopnst  18453  iocopnst  18454  iccpnfcnv  18458  phtpcer  18509  phtpcco2  18513  pcohtpylem  18533  pcohtpy  18534  pcopt  18536  pcopt2  18537  pcorevlem  18540  pcorev2  18542  pcophtb  18543  om1addcl  18547  pi1cpbl  18558  pi1grplem  18563  pi1inv  18566  pi1xfrf  18567  pi1xfr  18569  pi1xfrcnvlem  18570  pi1xfrcnv  18571  pi1cof  18573  pi1coghm  18575  cphphl  18623  cphreccllem  18630  cphsqrcl2  18638  tchclm  18678  tchcph  18683  lmcau  18754  bcthlem4  18765  minveclem4c  18805  minveclem2  18806  minveclem3b  18808  minveclem4  18812  minveclem6  18814  ivthicc  18834  ovolfsval  18846  ovollb2lem  18863  ovolshftlem1  18884  ovolscalem1  18888  ovolicc2lem2  18893  ovolicc2lem5  18896  ovolicopnf  18899  ioombl1lem1  18931  ioombl1lem3  18933  ioombl1lem4  18934  uniioovol  18950  uniioombllem2a  18953  uniioombllem2  18954  uniioombllem3a  18955  uniioombllem3  18956  uniioombllem4  18957  uniioombllem6  18959  vitalilem2  18980  vitalilem3  18981  vitalilem4  18982  i1ff  19047  itg2monolem1  19121  itgreval  19167  ibladd  19191  iblabslem  19198  itgspliticc  19207  itgsplitioo  19208  ditgcl  19224  ditgswap  19225  ditgsplitlem  19226  ditgsplit  19227  limcresi  19251  dvlip2  19358  dveq0  19363  dvcnvre  19382  dvfsumlem2  19390  ftc1a  19400  mpfind  19444  ply1rem  19565  facth1  19566  fta1glem1  19567  fta1glem2  19568  ig1pcl  19577  ig1pdvds  19578  plyrem  19701  facth  19702  vieta1lem1  19706  vieta1lem2  19707  aaliou3lem3  19740  aaliou3lem7  19745  pserulm  19814  psercnlem2  19816  psercn  19818  pserdvlem1  19819  pserdvlem2  19820  pserdv  19821  abelth2  19834  coseq00topi  19886  coseq0negpitopi  19887  cosordlem  19909  efif1olem1  19920  dvloglem  20011  loglesqr  20114  quart1  20168  quartlem2  20170  quartlem3  20171  quartlem4  20172  quart  20173  asinsinlem  20203  atanlogsublem  20227  atans2  20243  dvatan  20247  rlimcnp2  20277  divsqrsumlem  20290  ftalem5  20330  ftalem7  20332  basellem4  20337  basellem5  20338  perfectlem2  20485  dchrinv  20516  chpdifbndlem1  20718  pntibndlem2  20756  pntlema  20761  pntlemb  20762  pntlemg  20763  pntlemh  20764  pntlemn  20765  pntlemq  20766  pntlemr  20767  pntlemj  20768  pntlemf  20770  pntlemk  20771  pntlemo  20772  pntlemp  20775  pntleml  20776  abvcxp  20780  grpofo  20882  vcablo  21129  nvvc  21187  sspba  21319  sspg  21320  minvecolem2  21470  minvecolem4c  21474  minvecolem4  21475  minvecolem5  21476  minvecolem6  21477  eleigveccl  22555  xrofsup  23270  eliccelico  23285  elicoelioo  23286  xrge0iifhom  23334  rnlogbval  23417  rnlogbcl  23418  nnlogbexp  23421  logbrec  23422  baselsiga  23491  insiga  23513  measfrge0  23548  prob01  23631  probfinmeasbOLD  23646  subfacp1lem2a  23726  subfacp1lem2b  23727  subfacp1lem3  23728  subfacp1lem4  23729  subfacp1lem5  23730  sconpht2  23784  sconpi1  23785  cvxscon  23789  cvmlift2lem3  23851  cvmlift2lem5  23853  cvmlift2lem6  23854  cvmlift2lem7  23855  cvmlift2lem12  23860  cvmliftphtlem  23863  cvmliftpht  23864  cvmlift3lem2  23866  cvmlift3lem4  23868  cvmlift3lem5  23869  cvmlift3lem6  23870  eupacl  23899  ghomgrplem  24011  iblabsnclem  25014  preorel  25328  fldax1  25531  fldax2  25532  vecax1  25556  icccon3  25804  doma  25831  dedalg  25846  cmpmorp  25882  cmppfc1  25884  dualalg  25885  ehm  25894  vidfunid  25940  isbnd3  26611  heiborlem3  26640  iccbnd  26667  rngohomf  26700  idlss  26744  stoweidlem30  27882  stoweidlem31  27883  stoweidlem38  27890  stoweidlem44  27896  sigardiv  27954  sigarcol  27957  sharhght  27958  sigaradd  27959  cevathlem1  27960  cevathlem2  27961  cevath  27962  lshplss  29793  opoccl  30006  opococ  30007  oplecon3  30011  hloml  30169  lclkrslem1  32349  lclkrslem2  32350
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