Theorem simp2d 1143

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

Step	Hyp	Ref	Expression
1		3simp1d.1	. 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒 ∧ 𝜃))
2		simp2 1137	. 2 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜒)
3	1, 2	syl 17	1 ⊢ (𝜑 → 𝜒)

Syntax hints:   → wi 4   ∧ w3a 1086

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 207  df-an 396  df-3an 1088

This theorem is referenced by:  simp2bi  1146  f1dom3fv3dif  7246  f1dom3el3dif  7247  f1prex  7262  oeeui  8569  resixp  8909  domssex  9108  cantnflem1a  9645  cantnflem1d  9648  cantnflem3  9651  cantnflem4  9652  fpwwe2lem6  10596  canthnumlem  10608  canthp1lem2  10613  wun0  10678  lelttrdi  11343  supmullem2  12161  supmul  12162  ixxdisj  13328  ixxun  13329  ixxss1  13331  ixxss2  13332  ixxss12  13333  ixxub  13334  ixxlb  13335  ubioo  13345  elicore  13366  iccgelb  13370  iccss2  13385  icodisj  13444  xov1plusxeqvd  13466  fldiv  13829  immul  15109  sqrtge0  15230  sqrtrege0  15339  icco1  15513  ruclem2  16207  ruclem3  16208  ruclem8  16212  ruclem12  16216  gcddvds  16480  crth  16755  phimullem  16756  eulerthlem1  16758  eulerthlem2  16759  prmreclem3  16896  sectcan  17724  sectco  17725  sectmon  17751  monsect  17752  funcixp  17836  funcsect  17841  invfuc  17946  coapm  18040  catciso  18080  posasymb  18287  ipodrsima  18507  pstr2  18537  psdmrn  18539  psref  18540  mhmlin  18727  subm0cl  18745  eqger  19117  eqgcpbl  19121  gaorber  19247  orbstafun  19250  cayleyth  19352  pmtrrn2  19397  pmtrfinv  19398  dfod2  19501  sylow2blem1  19557  dprdf  19945  dprdff  19951  dprdfcl  19952  dprdsplit  19987  dpjcntz  19991  ablfac1a  20008  ablfac1b  20009  lmodvsdi  20798  lbssp  20993  2idlcpblrng  21188  mpff  22018  mpfaddcl  22019  mpfmulcl  22020  mpfind  22021  pf1rcl  22243  mpfpf1  22245  mdetunilem2  22507  mdetunilem5  22510  mdetunilem6  22511  chfacfisfcpmat  22749  pnfnei  23114  cnptop2  23137  lmcl  23191  lmcnp  23198  flimfil  23863  tlmlmod  24083  ustbasel  24101  ustincl  24102  ustinvel  24104  ustfilxp  24107  tusunif  24163  imasdsf1olem  24268  xmeter  24328  tmsds  24379  metustexhalf  24451  nlmlmod  24573  qdensere  24664  blcvx  24693  tgqioo  24695  icccmplem2  24719  reconnlem1  24722  cnmpopc  24829  phtpcer  24901  phtpcco2  24906  pcohtpylem  24926  pcohtpy  24927  pcophtb  24936  om1addcl  24940  pi1blem  24946  pi1cpbl  24951  pi1grplem  24956  pi1inv  24959  pi1xfrf  24960  pi1xfr  24962  pi1xfrcnvlem  24963  pi1cof  24966  pi1coghm  24968  cphnlm  25079  cphsqrtcl2  25093  tcphcph  25144  lmcau  25220  bcthlem4  25234  minveclem4c  25332  minveclem2  25333  minveclem3b  25335  minveclem4  25339  minveclem6  25341  ivthicc  25366  ovolfsval  25378  ovollb2lem  25396  ovolshftlem1  25417  ovolscalem1  25421  ovolicc1  25424  ovolicc2lem2  25426  ovolicc2lem4  25428  ovolicc2lem5  25429  ovolicopnf  25432  ioombl1lem1  25466  ioombl1lem3  25468  ioombl1lem4  25469  uniioovol  25487  uniioombllem2a  25490  uniioombllem2  25491  uniioombllem3a  25492  uniioombllem3  25493  uniioombllem4  25494  uniioombllem6  25496  dyadmaxlem  25505  volivth  25515  vitalilem2  25517  vitalilem5  25520  i1frn  25585  itg2monolem1  25658  itgcnlem  25698  itgrevallem1  25703  itgreval  25705  itgle  25718  ibladd  25729  iblabslem  25736  itgspliticc  25745  itgsplitioo  25746  ditgcl  25766  ditgswap  25767  ditgsplitlem  25768  limcdif  25784  limcresi  25793  limccnp  25799  limccnp2  25800  limcco  25801  dvlip  25905  dvlip2  25907  dveq0  25912  dvgt0lem1  25914  dvivthlem1  25920  dvcnvrelem1  25929  dvcnvre  25931  dvfsumlem2  25940  dvfsumlem2OLD  25941  ftc1lem1  25949  ftc1a  25951  ftc1lem4  25953  ftc2ditglem  25959  itgsubstlem  25962  ply1rem  26078  fta1glem1  26080  ig1pdvds  26092  plyrem  26220  facth  26221  fta1lem  26222  vieta1lem1  26225  vieta1lem2  26226  aaliou3lem3  26259  aaliou3lem4  26261  aaliou3lem7  26264  taylfvallem1  26271  tayl0  26276  taylply2  26282  taylply2OLD  26283  radcnvle  26336  psercnlem2  26341  psercnlem1  26342  psercn  26343  pserdvlem1  26344  pserdvlem2  26345  abelth2  26359  coseq00topi  26418  coseq0negpitopi  26419  cosordlem  26446  tanord1  26453  efif1olem1  26458  loglesqrt  26678  logreclem  26679  relogbval  26689  nnlogbexp  26698  chordthmlem4  26752  quart1  26773  quartlem2  26775  quartlem3  26776  quartlem4  26777  quart  26778  acosbnd  26817  atancj  26827  atanlogsublem  26832  atantan  26840  atanbndlem  26842  dvatan  26852  atantayl  26854  rlimcnp2  26883  divsqrtsumlem  26897  ftalem5  26994  ftalem7  26996  basellem4  27001  basellem5  27002  perfectlem2  27148  dchrinv  27179  chpdifbndlem1  27471  pntibndlem2  27509  pntlemc  27513  pntlema  27514  pntlemb  27515  pntlemg  27516  pntlemh  27517  pntlemq  27519  pntlemr  27520  pntlemj  27521  pntlemi  27522  pntlemf  27523  pntlemk  27524  pntlemo  27525  pntleme  27526  pntlem3  27527  pntleml  27529  abvcxp  27533  scutun12  27729  slerec  27738  cofcut2  27837  cofcutr  27839  cofcutrtime  27842  cutmax  27849  cutmin  27850  addsproplem4  27886  addsproplem6  27888  addsuniflem  27915  addsasslem1  27917  addsasslem2  27918  negsproplem5  27945  negsproplem6  27946  negscut2  27953  negsunif  27968  mulsproplem12  28037  ssltmul1  28057  ssltmul2  28058  mulsuniflem  28059  precsexlem11  28126  twocut  28316  axtgpasch  28401  cgr3simp2  28455  legso  28533  hlne2  28540  hlln  28541  mirhl  28613  inagswap  28775  inagne2  28777  dfcgrg2  28797  subumgredg2  29219  upgrres1  29247  nb3grprlem1  29314  wlkp  29551  wspthsswwlkn  29855  2wlkdlem6  29868  clwwisshclwwsn  29952  erclwwlkeqlen  29955  erclwwlksym  29957  erclwwlktr  29958  clwwlkn  29962  clwwlknwrd  29970  clwwlknonex2e  30046  grpoass  30439  vcsm  30498  nvf  30596  ssps  30666  minvecolem2  30811  minvecolem4c  30815  minvecolem4  30816  minvecolem5  30817  minvecolem6  30818  eigvec1  31898  eliccelico  32707  elicoelioo  32708  pmtrto1cl  33063  cyc3evpm  33114  slmdvsdi  33175  slmdvs1  33180  sdrgdvcl  33256  sdrginvcl  33257  fldgenssp  33275  imaslmod  33331  prmidlnr  33417  qsidomlem2  33431  mxidlnr  33442  0ringmon1p  33533  irngnzply1lem  33692  irngnzply1  33693  ply1annig1p  33701  minplycl  33703  ply1annprmidl  33704  minplym1p  33710  minplynzm1p  33711  algextdeglem1  33714  algextdeglem2  33715  algextdeglem3  33716  algextdeglem4  33717  algextdeglem5  33718  constrsqrtcl  33776  cnre2csqlem  33907  lmxrge0  33949  sigaclci  34129  difelsiga  34130  insiga  34134  ldsysgenld  34157  sigapildsyslem  34158  sigapildsys  34159  ldgenpisyslem1  34160  measvnul  34203  sibfrn  34335  eulerpartlemt  34369  eulerpartlemmf  34373  tg5segofs  34671  lpadleft  34681  spthcycl  35123  subgrwlk  35126  acycgrcycl  35141  subfacp1lem2a  35174  subfacp1lem3  35176  subfacp1lem4  35177  subfacp1lem5  35178  sconnpht2  35232  sconnpi1  35233  resconn  35240  cvmsss  35261  cvmsn0  35262  cvmlift2lem3  35299  cvmlift2lem7  35303  cvmliftphtlem  35311  cvmliftpht  35312  cvmlift3lem5  35317  cvmlift3lem6  35318  msrf  35536  elmsta  35542  mclsax  35563  mthmpps  35576  mclspps  35578  ivthALT  36330  weiunpo  36460  weiunso  36461  weiunfr  36462  weiunse  36463  poimirlem17  37638  poimirlem20  37641  ibladdnc  37678  iblabsnclem  37684  ftc1cnnclem  37692  ftc1anc  37702  ftc2nc  37703  heiborlem3  37814  iccbnd  37841  rngohom1  37969  idl0cl  38019  maxidlnr  38043  lshpne  38982  opococ  39195  opexmid  39207  hlclat  39358  lclkrslem2  41539  fzne2d  41975  dvrelog2  42059  dvrelog3  42060  0nonelalab  42062  aks4d1p1p5  42070  primrootsunit1  42092  primrootscoprmpow  42094  primrootscoprbij  42097  primrootspoweq0  42101  aks6d1c2lem3  42121  aks6d1c2  42125  aks6d1c6lem5  42172  aks5lem1  42181  aks5lem2  42182  aks5lem3a  42184  aks5lem5a  42186  unitscyglem1  42190  evlsval3  42554  flt4lem5f  42652  flt4lem7  42654  nna4b4nsq  42655  gneispacern2  44135  cvgdvgrat  44309  iccshift  45523  iccsuble  45524  icoiccdif  45529  mullimc  45621  limccog  45625  mullimcf  45628  lptioo2  45636  limcmptdm  45640  limcicciooub  45642  xlimmnfvlem1  45837  xlimpnfvlem1  45841  icccncfext  45892  cncfioobdlem  45901  ditgeqiooicc  45965  itgsubsticc  45981  iblcncfioo  45983  itgiccshift  45985  itgperiod  45986  itgsbtaddcnst  45987  stoweidlem31  46036  stoweidlem36  46041  stoweidlem38  46043  stoweidlem44  46049  stoweidlem62  46067  dirkercncflem1  46108  dirkercncflem4  46111  fourierdlem26  46138  fourierdlem32  46144  fourierdlem33  46145  fourierdlem37  46149  fourierdlem42  46154  fourierdlem54  46165  fourierdlem63  46174  fourierdlem64  46175  fourierdlem65  46176  fourierdlem69  46180  fourierdlem74  46185  fourierdlem75  46186  fourierdlem79  46190  fourierdlem81  46192  fourierdlem82  46193  fourierdlem89  46200  fourierdlem90  46201  fourierdlem91  46202  fourierdlem93  46204  fourierdlem101  46212  fourierdlem111  46222  saldifcl  46324  unisalgen2  46359  hoidmv1lelem3  46598  smff  46737  sigardiv  46866  sigarcol  46869  sharhght  46870  sigaradd  46871  cevathlem1  46872  cevathlem2  46873  cevath  46874  proththd  47619  perfectALTVlem2  47727  gpgnbgrvtx0  48069  gpgnbgrvtx1  48070  imasubc2  49145  imaf1co  49148  idfullsubc  49154  fucofulem1  49303