Theorem simp3d 1010

Description: Deduce a conjunct from a triple conjunction. (Contributed by NM, 4-Sep-2005.)

Hypothesis

Ref	Expression
3simp1d.1

Assertion

Ref	Expression
simp3d

Proof of Theorem simp3d

Step	Hyp	Ref	Expression
1		3simp1d.1	. 2
2		simp3 998	. 2
3	1, 2	syl 16	1

Syntax hints:  ->wi 4  /\w3a 973

This theorem is referenced by:  simp3bi  1013  f1dom3fv3dif  6175  f1dom3el3dif  6176  oeeui  7270  erinxp  7404  resixp  7524  domssex2  7697  cantnflem1c  8127  cantnflem1  8129  cantnflem3  8131  cantnflem4  8132  cantnflem1cOLD  8150  cantnflem1OLD  8152  cantnflem3OLD  8153  cantnflem4OLD  8154  fpwwe2lem7  9035  canthnumlem  9047  canthp1lem2  9052  wununi  9105  wunpw  9106  wunpr  9108  ixxdisj  11573  ixxun  11574  ixxss1  11576  ixxss2  11577  ixxss12  11578  ixxub  11579  ixxlb  11580  lbioo  11589  iccsupr  11646  icodisj  11674  xov1plusxeqvd  11695  intfracq  11986  fldiv  11987  seqf1olem2  12147  cjmul  12975  icco1  13363  rpnnen2lem10  13957  ruclem2  13965  ruclem3  13966  ruclem9  13971  ruclem12  13974  dvdslegcd  14154  crt  14308  eulerthlem1  14311  eulerthlem2  14312  pcpremul  14367  prmreclem2  14435  prmreclem3  14436  4sqlem13  14475  sectcan  15150  sectco  15151  sectmon  15172  monsect  15173  funcid  15239  funcco  15240  funcsect  15241  invfuc  15343  fuciso  15344  coapm  15398  catciso  15434  postr  15583  ipodrsima  15795  psref2  15834  psasym  15840  mhm0  15974  submcl  15984  submmnd  15985  eqger  16251  eqgcpbl  16255  gaorber  16346  orbsta  16351  cayleyth  16440  pmtrrn2  16485  pmtrfinv  16486  pmtrfmvdn0  16487  dfod2  16586  sylow2blem1  16640  sylow2blem3  16642  dprdcntz  17041  dprddisj  17042  dprdffsupp  17048  dprdffiOLD  17054  dpjdisj  17102  ablfac1a  17120  ablfac1b  17121  lmodvsdir  17536  lmhmlin  17681  lbsind  17726  2idlcpbl  17882  assasca  17970  mpfind  18205  mpt2frlmd  18808  mdetunilem2  19115  mdetunilem5  19118  mdetunilem6  19119  mnfnei  19722  cnprcl  19746  lmcvg  19763  lmff  19802  lmcls  19803  lmcnp  19805  fbasssin  20337  flimfil  20470  tgpconcomp  20611  tlmtrg  20692  ustssel  20708  ustincl  20710  ustdiag  20711  ustinvel  20712  ustexhalf  20713  ustfilxp  20715  tustopn  20774  tususp  20775  imasdsf1olem  20876  xmeter  20936  xmetresbl  20940  tmstopn  20988  metustexhalfOLD  21066  metustexhalf  21067  nlmnrg  21188  qdensere  21277  blcvx  21303  tgqioo  21305  icccmplem1  21327  icccmplem2  21328  reconnlem1  21331  cnmpt2pc  21428  iccpnfcnv  21444  phtpcer  21495  phtpcco2  21499  pcohtpy  21520  pcorev2  21528  pcophtb  21529  om1addcl  21533  pi1blem  21539  pi1cpbl  21544  pi1grplem  21549  pi1inv  21552  pi1xfrf  21553  pi1xfr  21555  pi1xfrcnvlem  21556  pi1cof  21559  pi1coghm  21561  cphreccllem  21625  cphsca  21626  cphsubrg  21627  cphsqrtcl2  21633  tchclm  21675  tchcph  21680  lmmcvg  21700  cmetcaulem  21727  lmcau  21751  bcthlem3  21765  bcthlem4  21766  minveclem4c  21840  minveclem2  21841  minveclem3b  21843  minveclem4  21847  minveclem6  21849  ivthicc  21870  ovollb2lem  21899  ovolshftlem1  21920  ovolscalem1  21924  ovolicc1  21927  ovolicc2lem2  21929  ovolicc2lem3  21930  ovolicc2lem4  21931  ovolicc2lem5  21932  ioombl1lem1  21968  dyadmaxlem  22006  volivth  22016  vitalilem2  22018  vitalilem4  22020  i1fima2  22086  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  limcres  22290  limccnp  22295  limccnp2  22296  limcun  22299  dvlip  22394  dvlip2  22396  dveq0  22401  dvgt0lem1  22403  dvivthlem1  22409  dvcnvrelem1  22418  dvcnvre  22420  dvfsumlem2  22428  ftc1lem1  22436  ftc1lem2  22437  ftc1a  22438  ftc1lem4  22440  ftc2  22445  ftc2ditglem  22446  itgsubstlem  22449  ply1rem  22564  fta1glem2  22567  ig1pdvds  22577  plyrem  22701  fta1lem  22703  vieta1lem2  22707  aaliou3lem3  22740  pserulm  22817  psercnlem2  22819  psercnlem1  22820  psercn  22821  pserdvlem1  22822  pserdvlem2  22823  abelth2  22837  coseq00topi  22895  coseq0negpitopi  22896  cosordlem  22918  tanord1  22924  efif1olem1  22929  dvloglem  23029  efopnlem1  23037  logreclem  23150  chordthmlem4  23166  quart1  23187  quartlem2  23189  quartlem3  23190  quart  23192  acosbnd  23231  atancj  23241  atanlogsublem  23246  atantan  23254  atanbndlem  23256  atans2  23262  dvatan  23266  atantayl  23268  divsqrtsumlem  23309  ftalem5  23350  basellem5  23358  ppisval  23377  chtleppi  23485  chpchtsum  23494  chpub  23495  mersenne  23502  perfectlem2  23505  dchrinv  23536  rplogsumlem2  23670  chpdifbndlem1  23738  pntibndlem2  23776  pntlema  23781  pntlemb  23782  pntlemg  23783  pntlemh  23784  pntlemr  23787  pntlemj  23788  pntlemf  23790  pntlemk  23791  pntlemo  23792  pntlemp  23795  pntleml  23796  abvcxp  23800  ostth2lem2  23819  axtgcont1  23865  cgr3simp3  23913  legso  23985  hlln  23991  hltr  23994  btwnhl  23998  mirhl  24059  mirbtwnhl  24060  opphllem4  24122  opphl  24125  wlkonwlk  24537  wwlksswrd  24688  wwlkeq  24722  clwwisshclwwn  24808  erclwwlksym  24814  erclwwlktr  24815  el2wlksoton  24878  el2spthsoton  24879  cusgraiffrusgra  24940  eupapf  24972  frrusgraord  25071  tncp  25180  grpolidinv  25203  nvs  25565  nvz  25572  nvtri  25573  sspn  25649  minvecolem2  25791  minvecolem4c  25795  minvecolem4  25796  minvecolem5  25797  minvecolem6  25798  adj1  26852  eliccelico  27588  elicoelioo  27589  slmdvsdir  27759  slmd0vs  27767  locfinreflem  27843  cnre2csqlem  27892  rnlogbval  28016  rnlogbcl  28017  nnlogbexp  28020  logbrec  28021  sigaclci  28132  unelsiga  28134  insiga  28137  measvun  28180  cntmeas  28197  sibfima  28280  signstfveq0  28534  tg5segofs  28553  subfacp1lem3  28626  subfacp1lem4  28627  subfacp1lem5  28628  sconpht2  28683  sconpi1  28684  txscon  28686  rescon  28691  cvmcn  28707  cvmsuni  28714  cvmsdisj  28715  cvmshmeo  28716  cvmlift2lem8  28755  cvmlift2lem13  28760  cvmliftphtlem  28762  cvmliftpht  28763  cvmlift3lem6  28769  msrf  28902  elmsta  28908  mthmpps  28942  mclsppslem  28943  ghomgrplem  29029  ibladdnc  30072  iblabsnclem  30078  ftc2nc  30099  dvasin  30103  ivthALT  30153  isbndx  30278  isbnd3  30280  prdsbnd  30289  heiborlem3  30309  iccbnd  30336  rngohomadd  30372  rngohommul  30373  idladdcl  30416  idllmulcl  30417  idlrmulcl  30418  maxidlmax  30440  pridlc  30468  acongrep  30918  cvgdvgrat  31194  binomcxplemdvbinom  31258  elicore  31537  eliocre  31547  iccshift  31558  iccsuble  31559  icoiccdif  31564  mullimc  31622  limccog  31626  limciccioolb  31627  mullimcf  31629  limcperiod  31634  lptioo2  31637  lptioo1  31638  neglimc  31653  addlimc  31654  0ellimcdiv  31655  reclimc  31659  icccncfext  31690  cncfioobdlem  31699  ditgeqiooicc  31759  iblspltprt  31772  iblcncfioo  31777  itgiccshift  31779  itgperiod  31780  itgsbtaddcnst  31781  stoweidlem11  31793  stoweidlem31  31813  stoweidlem36  31818  stoweidlem38  31820  stoweidlem62  31844  dirkercncflem1  31885  dirkercncflem4  31888  fourierdlem26  31915  fourierdlem32  31921  fourierdlem33  31922  fourierdlem37  31926  fourierdlem42  31931  fourierdlem54  31943  fourierdlem63  31952  fourierdlem64  31953  fourierdlem65  31954  fourierdlem74  31963  fourierdlem75  31964  fourierdlem79  31968  fourierdlem81  31970  fourierdlem82  31971  fourierdlem89  31978  fourierdlem90  31979  fourierdlem91  31980  fourierdlem93  31982  fourierdlem101  31990  fourierdlem107  31996  fourierdlem109  31998  fourierdlem111  32000  sigardiv  32078  sigarcol  32081  sharhght  32082  sigaradd  32083  cevathlem1  32084  cevathlem2  32085  cevath  32086  lelttrdi  32323  bnj1018  34020  lshpnelb  34709  lshpcmp  34713  oplecon3  34924  opnoncon  34933  hlcvl  35084  dochshpncl  37111  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