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

Theorem simp1d 1008
Description: Deduce a conjunct from a triple conjunction. (Contributed by NM, 4-Sep-2005.)
Hypothesis
Ref Expression
3simp1d.1
Assertion
Ref Expression
simp1d

Proof of Theorem simp1d
StepHypRef Expression
1 3simp1d.1 . 2
2 simp1 996 . 2
31, 2syl 16 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\w3a 973
This theorem is referenced by:  simp1bi  1011  f1dom3fv3dif  6175  f1dom3el3dif  6176  oeeui  7270  oeeu  7271  erinxp  7404  domssex2  7697  domssex  7698  cantnflem1a  8125  cantnflem1b  8126  cantnflem1c  8127  cantnflem1d  8128  cantnflem1  8129  cantnflem3  8131  cantnflem4  8132  cantnflem1aOLD  8148  cantnflem1bOLD  8149  cantnflem1cOLD  8150  cantnflem1dOLD  8151  cantnflem1OLD  8152  cantnflem3OLD  8153  cantnflem4OLD  8154  fpwwe2lem7  9035  canthnumlem  9047  canthp1lem2  9052  wuntr  9104  supmul1  10533  supmullem1  10534  supmullem2  10535  supmul  10536  ixxdisj  11573  ixxun  11574  ixxss1  11576  ixxss2  11577  ixxss12  11578  ixxub  11579  ixxlb  11580  iccss2  11624  iocssre  11633  icossre  11634  iccssre  11635  icodisj  11674  iccf1o  11693  xov1plusxeqvd  11695  fzen  11732  intfracq  11986  fldiv  11987  remul  12962  sqrlem6  13081  resqrtth  13089  sqrtth  13197  ruclem6  13968  ruclem9  13971  ruclem12  13974  gcdn0cl  14152  crt  14308  phimullem  14309  eulerthlem1  14311  eulerthlem2  14312  pcpremul  14367  prmreclem3  14436  sectcan  15150  sectco  15151  sectmon  15172  monsect  15173  funcf1  15235  funcsect  15241  invfuc  15343  coapm  15398  catciso  15434  posrefOLD  15581  psrel  15833  pstr  15841  mhmf  15971  submss  15981  eqger  16251  eqgcpbl  16255  gaorber  16346  orbstafun  16349  cayleyth  16440  dprdgrp  17038  dprdff  17046  dprdffOLD  17052  ablfac1a  17120  ablfac1b  17121  lmodvscl  17529  lbsss  17723  2idlcpbl  17882  assalmod  17968  mpfind  18205  mdetunilem2  19115  mdetunilem5  19118  mdetunilem6  19119  chfacfisfcpmat  19356  cnptop1  19743  lmfpm  19796  lmff  19802  lmcnp  19805  flimtop  20466  tlmtmd  20689  ustssxp  20707  ustdiag  20711  ustfilxp  20715  ustbas2  20728  tusbas  20771  imasdsf1olem  20876  xmeter  20936  tmsbas  20986  metustexhalfOLD  21066  metustexhalf  21067  nlmngp  21186  qdensere  21277  blcvx  21303  tgqioo  21305  icccmplem2  21328  reconnlem1  21331  cnmpt2pc  21428  icoopnst  21439  iocopnst  21440  iccpnfcnv  21444  phtpcer  21495  phtpcco2  21499  pcohtpylem  21519  pcohtpy  21520  pcopt  21522  pcopt2  21523  pcorevlem  21526  pcorev2  21528  pcophtb  21529  om1addcl  21533  pi1cpbl  21544  pi1grplem  21549  pi1inv  21552  pi1xfrf  21553  pi1xfr  21555  pi1xfrcnvlem  21556  pi1xfrcnv  21557  pi1cof  21559  pi1coghm  21561  cphphl  21618  cphreccllem  21625  cphsqrtcl2  21633  tchclm  21675  tchcph  21680  lmcau  21751  bcthlem4  21766  minveclem4c  21840  minveclem2  21841  minveclem3b  21843  minveclem4  21847  minveclem6  21849  ivthicc  21870  ovolfsval  21882  ovollb2lem  21899  ovolshftlem1  21920  ovolscalem1  21924  ovolicc2lem2  21929  ovolicc2lem5  21932  ovolicopnf  21935  ioombl1lem1  21968  ioombl1lem3  21970  ioombl1lem4  21971  uniioovol  21988  uniioombllem2a  21991  uniioombllem2  21992  uniioombllem3a  21993  uniioombllem3  21994  uniioombllem4  21995  uniioombllem6  21997  vitalilem2  22018  vitalilem3  22019  vitalilem4  22020  i1ff  22083  itg2monolem1  22157  itgreval  22203  ibladd  22227  iblabslem  22234  itgspliticc  22243  itgsplitioo  22244  ditgcl  22262  ditgswap  22263  ditgsplitlem  22264  ditgsplit  22265  limcresi  22289  dvlip2  22396  dveq0  22401  dvcnvre  22420  dvfsumlem2  22428  ftc1a  22438  ply1rem  22564  facth1  22565  fta1glem1  22566  fta1glem2  22567  ig1pcl  22576  ig1pdvds  22577  plyrem  22701  facth  22702  vieta1lem1  22706  vieta1lem2  22707  aaliou3lem3  22740  aaliou3lem7  22745  pserulm  22817  psercnlem2  22819  psercn  22821  pserdvlem1  22822  pserdvlem2  22823  pserdv  22824  abelth2  22837  coseq00topi  22895  coseq0negpitopi  22896  cosordlem  22918  efif1olem1  22929  dvloglem  23029  loglesqrt  23132  quart1  23187  quartlem2  23189  quartlem3  23190  quartlem4  23191  quart  23192  asinsinlem  23222  atanlogsublem  23246  atans2  23262  dvatan  23266  rlimcnp2  23296  divsqrtsumlem  23309  ftalem5  23350  ftalem7  23352  basellem4  23357  basellem5  23358  perfectlem2  23505  dchrinv  23536  chpdifbndlem1  23738  pntibndlem2  23776  pntlema  23781  pntlemb  23782  pntlemg  23783  pntlemh  23784  pntlemn  23785  pntlemq  23786  pntlemr  23787  pntlemj  23788  pntlemf  23790  pntlemk  23791  pntlemo  23792  pntlemp  23795  pntleml  23796  abvcxp  23800  axtgbtwnid  23863  cgr3simp1  23911  hlne1  23989  hltr  23994  btwnhl  23998  mirhl  24059  opphllem4  24122  wwlksubclwwlk  24804  clwwnisshclwwn  24809  rusisusgra  24931  eupacl  24969  grpofo  25201  vcablo  25450  nvvc  25508  sspba  25640  sspg  25641  minvecolem2  25791  minvecolem4c  25795  minvecolem4  25796  minvecolem5  25797  minvecolem6  25798  eleigveccl  26878  xrofsup  27582  eliccelico  27588  elicoelioo  27589  slmdvscl  27757  slmdvsass  27760  rnlogbval  28016  rnlogbcl  28017  nnlogbexp  28020  logbrec  28021  baselsiga  28115  insiga  28137  measfrge0  28174  sibfmbl  28277  eulerpartlemt  28310  eulerpartlemmf  28314  probfinmeasbOLD  28367  tg5segofs  28553  subfacp1lem2a  28624  subfacp1lem2b  28625  subfacp1lem3  28626  subfacp1lem4  28627  subfacp1lem5  28628  sconpht2  28683  sconpi1  28684  cvxscon  28688  cvmlift2lem3  28750  cvmlift2lem5  28752  cvmlift2lem6  28753  cvmlift2lem7  28754  cvmlift2lem12  28759  cvmliftphtlem  28762  cvmliftpht  28763  cvmlift3lem2  28765  cvmlift3lem4  28767  cvmlift3lem5  28768  cvmlift3lem6  28769  msrf  28902  elmsta  28908  mthmpps  28942  mclsppslem  28943  mclspps  28944  ghomgrplem  29029  iblabsnclem  30078  dvasin  30103  isbnd3  30280  heiborlem3  30309  iccbnd  30336  rngohomf  30369  idlss  30413  eliccre  31540  eliocre  31547  icoiccdif  31564  limccog  31626  lptioo1  31638  cncfiooicclem1  31696  cncfioobdlem  31699  ditgeqiooicc  31759  stoweidlem30  31812  stoweidlem31  31813  stoweidlem38  31820  stoweidlem44  31826  fourierdlem26  31915  fourierdlem32  31921  fourierdlem33  31922  fourierdlem37  31926  fourierdlem42  31931  fourierdlem54  31943  fourierdlem63  31952  fourierdlem64  31953  fourierdlem65  31954  fourierdlem69  31958  fourierdlem79  31968  fourierdlem82  31971  fourierdlem89  31978  fourierdlem90  31979  fourierdlem91  31980  fourierdlem111  32000  sigardiv  32078  sigarcol  32081  sharhght  32082  sigaradd  32083  cevathlem1  32084  cevathlem2  32085  cevath  32086  lelttrdi  32323  lshplss  34706  opoccl  34919  opococ  34920  oplecon3  34924  hloml  35082  lclkrslem1  37264  lclkrslem2  37265
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 975
  Copyright terms: Public domain W3C validator