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

Theorem simp1d 1026
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 1014 . 2  |-  ( ( ps  /\  ch  /\  th )  ->  ps )
31, 2syl 17 1  |-  ( ph  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ w3a 991
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 190  df-an 377  df-3an 993
This theorem is referenced by:  simp1bi  1029  f1dom3fv3dif  6193  f1dom3el3dif  6194  f1prex  6207  oeeui  7329  oeeu  7330  erinxp  7463  domssex2  7758  domssex  7759  cantnflem1a  8216  cantnflem1b  8217  cantnflem1c  8218  cantnflem1d  8219  cantnflem1  8220  cantnflem3  8222  cantnflem4  8223  fpwwe2lem7  9087  canthnumlem  9099  canthp1lem2  9104  wuntr  9156  supmul1  10604  supmullem1  10605  supmullem2  10606  supmul  10607  ixxdisj  11679  ixxun  11680  ixxss1  11682  ixxss2  11683  ixxss12  11684  ixxub  11685  ixxlb  11686  ixxlbOLD  11687  iccss2  11734  iocssre  11743  icossre  11744  iccssre  11745  icodisj  11786  iccf1o  11805  xov1plusxeqvd  11807  fzen  11845  intfracq  12118  fldiv  12119  remul  13241  sqrlem6  13360  resqrtth  13368  sqrtth  13476  ruclem6  14336  ruclem9  14339  ruclem12  14342  gcdn0cl  14525  crt  14775  phimullem  14776  eulerthlem1  14778  eulerthlem2  14779  pcpremul  14842  prmreclem3  14911  sectcan  15709  sectco  15710  sectmon  15736  monsect  15737  funcf1  15820  funcsect  15826  invfuc  15928  coapm  16015  catciso  16051  posrefOLD  16246  psrel  16498  pstr  16506  mhmf  16636  submss  16646  eqger  16916  eqgcpbl  16920  gaorber  17011  orbstafun  17014  cayleyth  17105  dprdgrp  17686  dprdff  17694  ablfac1a  17751  ablfac1b  17752  lmodvscl  18157  lbsss  18349  2idlcpbl  18507  assalmod  18592  mpfind  18808  mdetunilem2  19687  mdetunilem5  19690  mdetunilem6  19691  chfacfisfcpmat  19928  cnptop1  20307  lmfpm  20360  lmff  20366  lmcnp  20369  flimtop  21029  tlmtmd  21250  ustssxp  21268  ustdiag  21272  ustfilxp  21276  ustbas2  21289  tusbas  21332  imasdsf1olem  21437  xmeter  21497  tmsbas  21547  metustexhalf  21620  nlmngp  21729  qdensere  21839  blcvx  21865  tgqioo  21867  icccmplem2  21890  reconnlem1  21893  cnmpt2pc  22005  icoopnst  22016  iocopnst  22017  iccpnfcnv  22021  phtpcer  22075  phtpcco2  22079  pcohtpylem  22099  pcohtpy  22100  pcopt  22102  pcopt2  22103  pcorevlem  22106  pcorev2  22108  pcophtb  22109  om1addcl  22113  pi1cpbl  22124  pi1grplem  22129  pi1inv  22132  pi1xfrf  22133  pi1xfr  22135  pi1xfrcnvlem  22136  pi1xfrcnv  22137  pi1cof  22139  pi1coghm  22141  cphphl  22198  cphreccllem  22205  cphsqrtcl2  22213  tchclm  22255  tchcph  22260  lmcau  22331  bcthlem4  22344  minveclem4c  22416  minveclem2  22417  minveclem3b  22419  minveclem4  22423  minveclem6  22425  minveclem4cOLD  22428  minveclem2OLD  22429  minveclem3bOLD  22431  minveclem4OLD  22435  minveclem6OLD  22437  ivthicc  22458  ovolfsval  22472  ovollb2lem  22490  ovolshftlem1  22511  ovolscalem1  22515  ovolicc2lem2  22520  ovolicc2lem5  22524  ovolicopnf  22527  ioombl1lem1  22560  ioombl1lem3  22562  ioombl1lem4  22563  uniioovol  22585  uniioombllem2a  22588  uniioombllem2  22589  uniioombllem2OLD  22590  uniioombllem3a  22591  uniioombllem3  22592  uniioombllem4  22593  uniioombllem6  22595  vitalilem2  22616  vitalilem3  22617  vitalilem4  22618  i1ff  22683  itg2monolem1  22757  itgreval  22803  ibladd  22827  iblabslem  22834  itgspliticc  22843  itgsplitioo  22844  ditgcl  22862  ditgswap  22863  ditgsplitlem  22864  ditgsplit  22865  limcresi  22889  dvlip2  22996  dveq0  23001  dvcnvre  23020  dvfsumlem2  23028  ftc1a  23038  ply1rem  23163  facth1  23164  fta1glem1  23165  fta1glem2  23166  ig1pcl  23176  ig1pdvds  23177  ig1pclOLD  23182  ig1pdvdsOLD  23183  plyrem  23307  facth  23308  vieta1lem1  23312  vieta1lem2  23313  aaliou3lem3  23349  aaliou3lem7  23354  pserulm  23426  psercnlem2  23428  psercn  23430  pserdvlem1  23431  pserdvlem2  23432  pserdv  23433  abelth2  23446  coseq00topi  23506  coseq0negpitopi  23507  cosordlem  23529  efif1olem1  23540  dvloglem  23642  loglesqrt  23747  relogbval  23758  nnlogbexp  23767  logbrec  23768  quart1  23831  quartlem2  23833  quartlem3  23834  quartlem4  23835  quart  23836  asinsinlem  23866  atanlogsublem  23890  atans2  23906  dvatan  23910  rlimcnp2  23941  divsqrtsumlem  23954  ftalem5  24050  ftalem5OLD  24052  ftalem7  24054  basellem4  24059  basellem5  24060  perfectlem2  24207  dchrinv  24238  chpdifbndlem1  24440  pntibndlem2  24478  pntlema  24483  pntlemb  24484  pntlemg  24485  pntlemh  24486  pntlemn  24487  pntlemq  24488  pntlemr  24489  pntlemj  24490  pntlemf  24492  pntlemk  24493  pntlemo  24494  pntlemp  24497  pntleml  24498  abvcxp  24502  axtgbtwnid  24563  cgr3simp1  24614  hlne1  24699  hltr  24704  btwnhl  24708  mirhl  24773  opphllem4  24841  hlpasch  24847  inagswap  24929  wwlksubclwwlk  25581  clwwnisshclwwn  25586  rusisusgra  25708  eupacl  25746  grpofo  25976  vcablo  26225  nvvc  26283  sspba  26415  sspg  26416  minvecolem2  26566  minvecolem4c  26570  minvecolem4  26571  minvecolem5  26572  minvecolem6  26573  minvecolem2OLD  26576  minvecolem4cOLD  26580  minvecolem4OLD  26581  minvecolem5OLD  26582  minvecolem6OLD  26583  eleigveccl  27661  xrofsup  28402  eliccelico  28408  elicoelioo  28409  slmdvscl  28579  slmdvsass  28582  baselsiga  28986  insiga  29008  ldsysgenld  29031  sigapildsys  29033  ldgenpisyslem1  29034  measfrge0  29074  sibfmbl  29217  eulerpartlemt  29253  eulerpartlemmf  29257  probfinmeasbOLD  29310  tg5segofs  29539  subfacp1lem2a  29952  subfacp1lem2b  29953  subfacp1lem3  29954  subfacp1lem4  29955  subfacp1lem5  29956  sconpht2  30010  sconpi1  30011  cvxscon  30015  cvmlift2lem3  30077  cvmlift2lem5  30079  cvmlift2lem6  30080  cvmlift2lem7  30081  cvmlift2lem12  30086  cvmliftphtlem  30089  cvmliftpht  30090  cvmlift3lem2  30092  cvmlift3lem4  30094  cvmlift3lem5  30095  cvmlift3lem6  30096  msrf  30229  elmsta  30235  mthmpps  30269  mclsppslem  30270  mclspps  30271  ghomgrplem  30356  iblabsnclem  32050  dvasin  32073  isbnd3  32161  heiborlem3  32190  iccbnd  32217  rngohomf  32250  idlss  32294  lshplss  32592  opoccl  32805  opococ  32806  oplecon3  32810  hloml  32968  lclkrslem1  35150  lclkrslem2  35151  eliccre  37641  eliocre  37647  icoiccdif  37663  limccog  37738  lptioo1  37750  cncfiooicclem1  37809  cncfioobdlem  37812  ditgeqiooicc  37875  stoweidlem30  37929  stoweidlem31  37930  stoweidlem38  37937  stoweidlem44  37943  fourierdlem26  38033  fourierdlem32  38040  fourierdlem33  38041  fourierdlem37  38045  fourierdlem42  38050  fourierdlem42OLD  38051  fourierdlem54  38062  fourierdlem63  38071  fourierdlem64  38072  fourierdlem65  38073  fourierdlem69  38077  fourierdlem79  38087  fourierdlem82  38090  fourierdlem89  38097  fourierdlem90  38098  fourierdlem91  38099  fourierdlem111  38119  0sal  38219  hoidmv1lelem3  38453  sigardiv  38508  sigarcol  38511  sharhght  38512  sigaradd  38513  cevathlem1  38514  cevathlem2  38515  cevath  38516  perfectALTVlem2  38882  proththd  38952  lelttrdi  39089  1wlkvtxedg  39703  pthOnpth  39780  21wlkdlem6  39880  21wlkond  39886  2trlond  39888
  Copyright terms: Public domain W3C validator