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

Theorem simp1d 1007
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 995 . 2  |-  ( ( ps  /\  ch  /\  th )  ->  ps )
31, 2syl 16 1  |-  ( ph  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ w3a 972
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 974
This theorem is referenced by:  simp1bi  1010  f1dom3fv3dif  6156  f1dom3el3dif  6157  oeeui  7249  oeeu  7250  erinxp  7383  domssex2  7675  domssex  7676  cantnflem1a  8102  cantnflem1b  8103  cantnflem1c  8104  cantnflem1d  8105  cantnflem1  8106  cantnflem3  8108  cantnflem4  8109  cantnflem1aOLD  8125  cantnflem1bOLD  8126  cantnflem1cOLD  8127  cantnflem1dOLD  8128  cantnflem1OLD  8129  cantnflem3OLD  8130  cantnflem4OLD  8131  fpwwe2lem7  9012  canthnumlem  9024  canthp1lem2  9029  wuntr  9081  supmul1  10509  supmullem1  10510  supmullem2  10511  supmul  10512  ixxdisj  11548  ixxun  11549  ixxss1  11551  ixxss2  11552  ixxss12  11553  ixxub  11554  ixxlb  11555  iccss2  11599  iocssre  11608  icossre  11609  iccssre  11610  icodisj  11649  iccf1o  11668  xov1plusxeqvd  11670  fzen  11707  intfracq  11960  fldiv  11961  remul  12936  sqrlem6  13055  resqrtth  13063  sqrtth  13171  ruclem6  13840  ruclem9  13843  ruclem12  13846  gcdn0cl  14024  crt  14180  phimullem  14181  eulerthlem1  14183  eulerthlem2  14184  pcpremul  14239  prmreclem3  14308  sectcan  15022  sectco  15023  sectmon  15044  monsect  15045  funcf1  15104  funcsect  15110  invfuc  15212  coapm  15267  catciso  15303  posrefOLD  15449  psrel  15702  pstr  15710  mhmf  15840  submss  15850  eqger  16120  eqgcpbl  16124  gaorber  16215  orbstafun  16218  cayleyth  16309  dprdgrp  16907  dprdff  16914  dprdffOLD  16920  ablfac1a  16988  ablfac1b  16989  lmodvscl  17397  lbsss  17591  2idlcpbl  17750  assalmod  17836  mpfind  18073  mdetunilem2  18982  mdetunilem5  18985  mdetunilem6  18986  chfacfisfcpmat  19223  cnptop1  19609  lmfpm  19662  lmff  19668  lmcnp  19671  flimtop  20332  tlmtmd  20555  ustssxp  20573  ustdiag  20577  ustfilxp  20581  ustbas2  20594  tusbas  20637  imasdsf1olem  20742  xmeter  20802  tmsbas  20852  metustexhalfOLD  20932  metustexhalf  20933  nlmngp  21052  qdensere  21143  blcvx  21169  tgqioo  21171  icccmplem2  21194  reconnlem1  21197  cnmpt2pc  21294  icoopnst  21305  iocopnst  21306  iccpnfcnv  21310  phtpcer  21361  phtpcco2  21365  pcohtpylem  21385  pcohtpy  21386  pcopt  21388  pcopt2  21389  pcorevlem  21392  pcorev2  21394  pcophtb  21395  om1addcl  21399  pi1cpbl  21410  pi1grplem  21415  pi1inv  21418  pi1xfrf  21419  pi1xfr  21421  pi1xfrcnvlem  21422  pi1xfrcnv  21423  pi1cof  21425  pi1coghm  21427  cphphl  21484  cphreccllem  21491  cphsqrtcl2  21499  tchclm  21541  tchcph  21546  lmcau  21617  bcthlem4  21632  minveclem4c  21706  minveclem2  21707  minveclem3b  21709  minveclem4  21713  minveclem6  21715  ivthicc  21736  ovolfsval  21748  ovollb2lem  21765  ovolshftlem1  21786  ovolscalem1  21790  ovolicc2lem2  21795  ovolicc2lem5  21798  ovolicopnf  21801  ioombl1lem1  21834  ioombl1lem3  21836  ioombl1lem4  21837  uniioovol  21854  uniioombllem2a  21857  uniioombllem2  21858  uniioombllem3a  21859  uniioombllem3  21860  uniioombllem4  21861  uniioombllem6  21863  vitalilem2  21884  vitalilem3  21885  vitalilem4  21886  i1ff  21949  itg2monolem1  22023  itgreval  22069  ibladd  22093  iblabslem  22100  itgspliticc  22109  itgsplitioo  22110  ditgcl  22128  ditgswap  22129  ditgsplitlem  22130  ditgsplit  22131  limcresi  22155  dvlip2  22262  dveq0  22267  dvcnvre  22286  dvfsumlem2  22294  ftc1a  22304  ply1rem  22430  facth1  22431  fta1glem1  22432  fta1glem2  22433  ig1pcl  22442  ig1pdvds  22443  plyrem  22566  facth  22567  vieta1lem1  22571  vieta1lem2  22572  aaliou3lem3  22605  aaliou3lem7  22610  pserulm  22682  psercnlem2  22684  psercn  22686  pserdvlem1  22687  pserdvlem2  22688  pserdv  22689  abelth2  22702  coseq00topi  22760  coseq0negpitopi  22761  cosordlem  22783  efif1olem1  22794  dvloglem  22894  loglesqrt  22997  quart1  23052  quartlem2  23054  quartlem3  23055  quartlem4  23056  quart  23057  asinsinlem  23087  atanlogsublem  23111  atans2  23127  dvatan  23131  rlimcnp2  23161  divsqrtsumlem  23174  ftalem5  23215  ftalem7  23217  basellem4  23222  basellem5  23223  perfectlem2  23370  dchrinv  23401  chpdifbndlem1  23603  pntibndlem2  23641  pntlema  23646  pntlemb  23647  pntlemg  23648  pntlemh  23649  pntlemn  23650  pntlemq  23651  pntlemr  23652  pntlemj  23653  pntlemf  23655  pntlemk  23656  pntlemo  23657  pntlemp  23660  pntleml  23661  abvcxp  23665  axtgbtwnid  23728  cgr3simp1  23776  hlne1  23854  hltr  23859  btwnhl  23863  mirhl  23924  opphllem4  23987  wwlksubclwwlk  24669  clwwnisshclwwn  24674  rusisusgra  24796  eupacl  24834  grpofo  25066  vcablo  25315  nvvc  25373  sspba  25505  sspg  25506  minvecolem2  25656  minvecolem4c  25660  minvecolem4  25661  minvecolem5  25662  minvecolem6  25663  eleigveccl  26743  xrofsup  27447  eliccelico  27453  elicoelioo  27454  slmdvscl  27623  slmdvsass  27626  rnlogbval  27882  rnlogbcl  27883  nnlogbexp  27886  logbrec  27887  baselsiga  27981  insiga  28003  measfrge0  28040  sibfmbl  28143  eulerpartlemt  28176  eulerpartlemmf  28180  probfinmeasbOLD  28233  tg5segofs  28419  subfacp1lem2a  28490  subfacp1lem2b  28491  subfacp1lem3  28492  subfacp1lem4  28493  subfacp1lem5  28494  sconpht2  28549  sconpi1  28550  cvxscon  28554  cvmlift2lem3  28616  cvmlift2lem5  28618  cvmlift2lem6  28619  cvmlift2lem7  28620  cvmlift2lem12  28625  cvmliftphtlem  28628  cvmliftpht  28629  cvmlift3lem2  28631  cvmlift3lem4  28633  cvmlift3lem5  28634  cvmlift3lem6  28635  msrf  28768  elmsta  28774  mthmpps  28808  mclsppslem  28809  mclspps  28810  ghomgrplem  28895  iblabsnclem  30046  dvasin  30071  isbnd3  30248  heiborlem3  30277  iccbnd  30304  rngohomf  30337  idlss  30381  eliccre  31472  eliocre  31479  icoiccdif  31496  limccog  31530  lptioo1  31542  cncfiooicclem1  31599  cncfioobdlem  31602  ditgeqiooicc  31645  stoweidlem30  31697  stoweidlem31  31698  stoweidlem38  31705  stoweidlem44  31711  fourierdlem26  31800  fourierdlem32  31806  fourierdlem33  31807  fourierdlem37  31811  fourierdlem42  31816  fourierdlem54  31828  fourierdlem63  31837  fourierdlem64  31838  fourierdlem65  31839  fourierdlem69  31843  fourierdlem79  31853  fourierdlem82  31856  fourierdlem89  31863  fourierdlem90  31864  fourierdlem91  31865  fourierdlem111  31885  sigardiv  31912  sigarcol  31915  sharhght  31916  sigaradd  31917  cevathlem1  31918  cevathlem2  31919  cevath  31920  lelttrdi  32157  lshplss  34408  opoccl  34621  opococ  34622  oplecon3  34626  hloml  34784  lclkrslem1  36966  lclkrslem2  36967
  Copyright terms: Public domain W3C validator