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

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

Proof of Theorem simp2d
StepHypRef Expression
1 3simp1d.1 . 2
2 simp2 997 . 2
31, 2syl 16 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\w3a 973
This theorem is referenced by:  simp2bi  1012  f1dom3fv3dif  6175  f1dom3el3dif  6176  oeeui  7270  erinxp  7404  resixp  7524  domssex  7698  cantnflem1a  8125  cantnflem1d  8128  cantnflem3  8131  cantnflem4  8132  cantnflem1aOLD  8148  cantnflem1dOLD  8151  cantnflem3OLD  8153  cantnflem4OLD  8154  fpwwe2lem7  9035  canthnumlem  9047  canthp1lem2  9052  wun0  9117  supmullem2  10535  supmul  10536  ixxdisj  11573  ixxun  11574  ixxss1  11576  ixxss2  11577  ixxss12  11578  ixxub  11579  ixxlb  11580  ubioo  11590  iccgelb  11610  iccss2  11624  icodisj  11674  xov1plusxeqvd  11695  fldiv  11987  immul  12969  sqrtge0  13091  sqrtrege0  13198  icco1  13363  ruclem2  13965  ruclem3  13966  ruclem8  13970  ruclem12  13974  gcddvds  14153  crt  14308  phimullem  14309  eulerthlem1  14311  eulerthlem2  14312  prmreclem3  14436  sectcan  15150  sectco  15151  sectmon  15172  monsect  15173  funcixp  15236  funcsect  15241  invfuc  15343  coapm  15398  catciso  15434  posasymb  15582  ipodrsima  15795  pstr2  15835  psdmrn  15837  psref  15838  mhmlin  15973  subm0cl  15983  eqger  16251  eqgcpbl  16255  gaorber  16346  orbstafun  16349  cayleyth  16440  pmtrrn2  16485  pmtrfinv  16486  dfod2  16586  sylow2blem1  16640  dprdf  17039  dprdff  17046  dprdfcl  17047  dprdffOLD  17052  dprdfclOLD  17053  dprdsplit  17097  dpjcntz  17101  ablfac1a  17120  ablfac1b  17121  lmodvsdi  17535  lbssp  17725  2idlcpbl  17882  assaring  17969  mpff  18202  mpfaddcl  18203  mpfmulcl  18204  mpfind  18205  pf1rcl  18385  mpfpf1  18387  mdetunilem2  19115  mdetunilem5  19118  mdetunilem6  19119  chfacfisfcpmat  19356  pnfnei  19721  cnptop2  19744  lmcl  19798  lmcnp  19805  flimfil  20470  tlmlmod  20691  ustbasel  20709  ustincl  20710  ustinvel  20712  ustfilxp  20715  tusunif  20772  imasdsf1olem  20876  xmeter  20936  tmsds  20987  metustexhalfOLD  21066  metustexhalf  21067  nlmlmod  21187  qdensere  21277  blcvx  21303  tgqioo  21305  icccmplem2  21328  reconnlem1  21331  cnmpt2pc  21428  phtpcer  21495  phtpcco2  21499  pcohtpylem  21519  pcohtpy  21520  pcophtb  21529  om1addcl  21533  pi1blem  21539  pi1cpbl  21544  pi1grplem  21549  pi1inv  21552  pi1xfrf  21553  pi1xfr  21555  pi1xfrcnvlem  21556  pi1cof  21559  pi1coghm  21561  cphnlm  21619  cphsqrtcl2  21633  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  ovolicc1  21927  ovolicc2lem2  21929  ovolicc2lem4  21931  ovolicc2lem5  21932  ovolicopnf  21935  ioombl1lem1  21968  ioombl1lem3  21970  ioombl1lem4  21971  uniioovol  21988  uniioombllem2a  21991  uniioombllem2  21992  uniioombllem3a  21993  uniioombllem3  21994  uniioombllem4  21995  uniioombllem6  21997  dyadmaxlem  22006  volivth  22016  vitalilem2  22018  vitalilem5  22021  i1frn  22084  itg2monolem1  22157  itgcnlem  22196  itgrevallem1  22201  itgreval  22203  itgle  22216  ibladd  22227  iblabslem  22234  itgspliticc  22243  itgsplitioo  22244  ditgcl  22262  ditgswap  22263  ditgsplitlem  22264  limcdif  22280  limcresi  22289  limccnp  22295  limccnp2  22296  limcco  22297  dvlip  22394  dvlip2  22396  dveq0  22401  dvgt0lem1  22403  dvivthlem1  22409  dvcnvrelem1  22418  dvcnvre  22420  dvfsumlem2  22428  ftc1lem1  22436  ftc1a  22438  ftc1lem4  22440  ftc2ditglem  22446  itgsubstlem  22449  ply1rem  22564  fta1glem1  22566  ig1pdvds  22577  plyrem  22701  facth  22702  fta1lem  22703  vieta1lem1  22706  vieta1lem2  22707  aaliou3lem3  22740  aaliou3lem4  22742  aaliou3lem7  22745  taylfvallem1  22752  tayl0  22757  taylply2  22763  radcnvle  22815  psercnlem2  22819  psercnlem1  22820  psercn  22821  pserdvlem1  22822  pserdvlem2  22823  abelth2  22837  coseq00topi  22895  coseq0negpitopi  22896  cosordlem  22918  tanord1  22924  efif1olem1  22929  loglesqrt  23132  logreclem  23150  chordthmlem4  23166  quart1  23187  quartlem2  23189  quartlem3  23190  quartlem4  23191  quart  23192  acosbnd  23231  atancj  23241  atanlogsublem  23246  atantan  23254  atanbndlem  23256  dvatan  23266  atantayl  23268  rlimcnp2  23296  divsqrtsumlem  23309  ftalem5  23350  ftalem7  23352  basellem4  23357  basellem5  23358  perfectlem2  23505  dchrinv  23536  chpdifbndlem1  23738  pntibndlem2  23776  pntlemc  23780  pntlema  23781  pntlemb  23782  pntlemg  23783  pntlemh  23784  pntlemq  23786  pntlemr  23787  pntlemj  23788  pntlemi  23789  pntlemf  23790  pntlemk  23791  pntlemo  23792  pntleme  23793  pntlem3  23794  pntleml  23796  abvcxp  23800  axtgpasch  23864  cgr3simp2  23912  legso  23985  hlne2  23990  hlln  23991  mirhl  24059  hlperpnel  24099  opphllem4  24122  wlkonwlk  24537  constr3pth  24660  vfwlkniswwlkn  24706  clwwlknscsh  24819  erclwwlknsym  24826  erclwwlkntr  24827  eupaf1o  24970  grpoass  25205  vcsm  25442  nvf  25561  ssps  25643  minvecolem2  25791  minvecolem4c  25795  minvecolem4  25796  minvecolem5  25797  minvecolem6  25798  eigvec1  26881  eliccelico  27588  elicoelioo  27589  slmdvsdi  27758  slmdvs1  27763  cnre2csqlem  27892  lmxrge0  27934  rnlogbval  28016  nnlogbexp  28020  sigaclci  28132  difelsiga  28133  insiga  28137  measvnul  28177  sibfrn  28279  eulerpartlemt  28310  eulerpartlemmf  28314  tg5segofs  28553  subfacp1lem2a  28624  subfacp1lem3  28626  subfacp1lem4  28627  subfacp1lem5  28628  sconpht2  28683  sconpi1  28684  rescon  28691  cvmsss  28712  cvmsn0  28713  cvmlift2lem3  28750  cvmlift2lem7  28754  cvmliftphtlem  28762  cvmliftpht  28763  cvmlift3lem5  28768  cvmlift3lem6  28769  msrf  28902  elmsta  28908  mclsax  28929  mthmpps  28942  mclspps  28944  ghomgrplem  29029  ghomfo  29031  ghomgsg  29033  ibladdnc  30072  iblabsnclem  30078  ftc1cnnclem  30088  ftc1anc  30098  ftc2nc  30099  ivthALT  30153  heiborlem3  30309  iccbnd  30336  rngohom1  30371  idl0cl  30415  maxidlnr  30439  cvgdvgrat  31194  elicore  31537  iccshift  31558  iccsuble  31559  icoiccdif  31564  mullimc  31622  limccog  31626  mullimcf  31629  lptioo2  31637  limcmptdm  31641  limcicciooub  31643  icccncfext  31690  cncfioobdlem  31699  ditgeqiooicc  31759  itgsubsticc  31775  iblcncfioo  31777  itgiccshift  31779  itgperiod  31780  itgsbtaddcnst  31781  stoweidlem11  31793  stoweidlem31  31813  stoweidlem36  31818  stoweidlem38  31820  stoweidlem44  31826  stoweidlem62  31844  dirkercncflem1  31885  dirkercncflem4  31888  fourierdlem26  31915  fourierdlem32  31921  fourierdlem33  31922  fourierdlem37  31926  fourierdlem42  31931  fourierdlem54  31943  fourierdlem63  31952  fourierdlem64  31953  fourierdlem65  31954  fourierdlem69  31958  fourierdlem74  31963  fourierdlem75  31964  fourierdlem79  31968  fourierdlem81  31970  fourierdlem82  31971  fourierdlem89  31978  fourierdlem90  31979  fourierdlem91  31980  fourierdlem93  31982  fourierdlem101  31990  fourierdlem111  32000  sigardiv  32078  sigarcol  32081  sharhght  32082  sigaradd  32083  cevathlem1  32084  cevathlem2  32085  cevath  32086  lelttrdi  32323  lshpne  34707  opococ  34920  opexmid  34932  hlclat  35083  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