Theorem simp2d 1144

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 1138	. 2 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜒)
3	1, 2	syl 17	1 ⊢ (𝜑 → 𝜒)

Syntax hints:   → wi 4   ∧ w3a 1087

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 1089

This theorem is referenced by:  simp2bi  1147  f1dom3fv3dif  7223  f1dom3el3dif  7224  f1prex  7239  oeeui  8538  resixp  8881  domssex  9076  cantnflem1a  9606  cantnflem1d  9609  cantnflem3  9612  cantnflem4  9613  fpwwe2lem6  10559  canthnumlem  10571  canthp1lem2  10576  wun0  10641  lelttrdi  11308  supmullem2  12127  supmul  12128  ixxdisj  13313  ixxun  13314  ixxss1  13316  ixxss2  13317  ixxss12  13318  ixxub  13319  ixxlb  13320  ubioo  13330  elicore  13351  iccgelb  13355  iccss2  13370  icodisj  13429  xov1plusxeqvd  13451  fldiv  13819  immul  15098  sqrtge0  15219  sqrtrege0  15328  icco1  15502  ruclem2  16199  ruclem3  16200  ruclem8  16204  ruclem12  16208  gcddvds  16472  crth  16748  phimullem  16749  eulerthlem1  16751  eulerthlem2  16752  prmreclem3  16889  sectcan  17722  sectco  17723  sectmon  17749  monsect  17750  funcixp  17834  funcsect  17839  invfuc  17944  coapm  18038  catciso  18078  posasymb  18285  ipodrsima  18507  pstr2  18537  psdmrn  18539  psref  18540  mhmlin  18761  subm0cl  18779  eqger  19153  eqgcpbl  19157  gaorber  19283  orbstafun  19286  cayleyth  19390  pmtrrn2  19435  pmtrfinv  19436  dfod2  19539  sylow2blem1  19595  dprdf  19983  dprdff  19989  dprdfcl  19990  dprdsplit  20025  dpjcntz  20029  ablfac1a  20046  ablfac1b  20047  lmodvsdi  20880  lbssp  21074  2idlcpblrng  21269  evlsval3  22067  mpff  22090  mpfaddcl  22091  mpfmulcl  22092  mpfind  22093  pf1rcl  22314  mpfpf1  22316  mdetunilem2  22578  mdetunilem5  22581  mdetunilem6  22582  chfacfisfcpmat  22820  pnfnei  23185  cnptop2  23208  lmcl  23262  lmcnp  23269  flimfil  23934  tlmlmod  24154  ustbasel  24172  ustincl  24173  ustinvel  24175  ustfilxp  24178  tusunif  24233  imasdsf1olem  24338  xmeter  24398  tmsds  24449  metustexhalf  24521  nlmlmod  24643  qdensere  24734  blcvx  24763  tgqioo  24765  icccmplem2  24789  reconnlem1  24792  cnmpopc  24895  phtpcer  24962  phtpcco2  24966  pcohtpylem  24986  pcohtpy  24987  pcophtb  24996  om1addcl  25000  pi1blem  25006  pi1cpbl  25011  pi1grplem  25016  pi1inv  25019  pi1xfrf  25020  pi1xfr  25022  pi1xfrcnvlem  25023  pi1cof  25026  pi1coghm  25028  cphnlm  25139  cphsqrtcl2  25153  tcphcph  25204  lmcau  25280  bcthlem4  25294  minveclem4c  25392  minveclem2  25393  minveclem3b  25395  minveclem4  25399  minveclem6  25401  ivthicc  25425  ovolfsval  25437  ovollb2lem  25455  ovolshftlem1  25476  ovolscalem1  25480  ovolicc1  25483  ovolicc2lem2  25485  ovolicc2lem4  25487  ovolicc2lem5  25488  ovolicopnf  25491  ioombl1lem1  25525  ioombl1lem3  25527  ioombl1lem4  25528  uniioovol  25546  uniioombllem2a  25549  uniioombllem2  25550  uniioombllem3a  25551  uniioombllem3  25552  uniioombllem4  25553  uniioombllem6  25555  dyadmaxlem  25564  volivth  25574  vitalilem2  25576  vitalilem5  25579  i1frn  25644  itg2monolem1  25717  itgcnlem  25757  itgrevallem1  25762  itgreval  25764  itgle  25777  ibladd  25788  iblabslem  25795  itgspliticc  25804  itgsplitioo  25805  ditgcl  25825  ditgswap  25826  ditgsplitlem  25827  limcdif  25843  limcresi  25852  limccnp  25858  limccnp2  25859  limcco  25860  dvlip  25960  dvlip2  25962  dveq0  25967  dvgt0lem1  25969  dvivthlem1  25975  dvcnvrelem1  25984  dvcnvre  25986  dvfsumlem2  25994  ftc1lem1  26002  ftc1a  26004  ftc1lem4  26006  ftc2ditglem  26012  itgsubstlem  26015  ply1rem  26131  fta1glem1  26133  ig1pdvds  26145  plyrem  26271  facth  26272  fta1lem  26273  vieta1lem1  26276  vieta1lem2  26277  aaliou3lem3  26310  aaliou3lem4  26312  aaliou3lem7  26315  taylfvallem1  26322  tayl0  26327  taylply2  26333  radcnvle  26385  psercnlem2  26389  psercnlem1  26390  psercn  26391  pserdvlem1  26392  pserdvlem2  26393  abelth2  26407  coseq00topi  26466  coseq0negpitopi  26467  cosordlem  26494  tanord1  26501  efif1olem1  26506  loglesqrt  26725  logreclem  26726  relogbval  26736  nnlogbexp  26745  chordthmlem4  26799  quart1  26820  quartlem2  26822  quartlem3  26823  quartlem4  26824  quart  26825  acosbnd  26864  atancj  26874  atanlogsublem  26879  atantan  26887  atanbndlem  26889  dvatan  26899  atantayl  26901  rlimcnp2  26930  divsqrtsumlem  26943  ftalem5  27040  ftalem7  27042  basellem4  27047  basellem5  27048  perfectlem2  27193  dchrinv  27224  chpdifbndlem1  27516  pntibndlem2  27554  pntlemc  27558  pntlema  27559  pntlemb  27560  pntlemg  27561  pntlemh  27562  pntlemq  27564  pntlemr  27565  pntlemj  27566  pntlemi  27567  pntlemf  27568  pntlemk  27569  pntlemo  27570  pntleme  27571  pntlem3  27572  pntleml  27574  abvcxp  27578  cutsun12  27782  lesrec  27791  eqcuts3  27796  cofcut2  27914  cofcutr  27916  cofcutrtime  27919  cutmax  27926  cutmin  27927  addsproplem4  27964  addsproplem6  27966  addsuniflem  27993  addsasslem1  27995  addsasslem2  27996  negsproplem5  28024  negsproplem6  28025  negcut2  28032  negsunif  28047  mulsproplem12  28119  sltmuls1  28139  sltmuls2  28140  mulsuniflem  28141  precsexlem11  28209  twocut  28415  pw2cut2  28454  axtgpasch  28535  cgr3simp2  28589  legso  28667  hlne2  28674  hlln  28675  mirhl  28747  inagswap  28909  inagne2  28911  dfcgrg2  28931  subumgredg2  29354  upgrres1  29382  nb3grprlem1  29449  wlkp  29685  wspthsswwlkn  29986  2wlkdlem6  29999  clwwisshclwwsn  30086  erclwwlkeqlen  30089  erclwwlksym  30091  erclwwlktr  30092  clwwlkn  30096  clwwlknwrd  30104  clwwlknonex2e  30180  grpoass  30574  vcsm  30633  nvf  30731  ssps  30801  minvecolem2  30946  minvecolem4c  30950  minvecolem4  30951  minvecolem5  30952  minvecolem6  30953  eigvec1  32033  eliccelico  32850  elicoelioo  32851  pmtrto1cl  33160  cyc3evpm  33211  slmdvsdi  33276  slmdvs1  33281  sdrgdvcl  33360  sdrginvcl  33361  fldgenssp  33379  imaslmod  33413  prmidlnr  33499  qsidomlem2  33513  mxidlnr  33524  0ringmon1p  33617  irngnzply1lem  33834  irngnzply1  33835  ply1annig1p  33848  minplycl  33850  ply1annprmidl  33851  minplym1p  33857  minplynzm1p  33858  algextdeglem1  33861  algextdeglem2  33862  algextdeglem3  33863  algextdeglem4  33864  algextdeglem5  33865  constrsqrtcl  33923  cnre2csqlem  34054  lmxrge0  34096  sigaclci  34276  difelsiga  34277  insiga  34281  ldsysgenld  34304  sigapildsyslem  34305  sigapildsys  34306  ldgenpisyslem1  34307  measvnul  34350  sibfrn  34481  eulerpartlemt  34515  eulerpartlemmf  34519  tg5segofs  34817  lpadleft  34827  spthcycl  35311  subgrwlk  35314  acycgrcycl  35329  subfacp1lem2a  35362  subfacp1lem3  35364  subfacp1lem4  35365  subfacp1lem5  35366  sconnpht2  35420  sconnpi1  35421  resconn  35428  cvmsss  35449  cvmsn0  35450  cvmlift2lem3  35487  cvmlift2lem7  35491  cvmliftphtlem  35499  cvmliftpht  35500  cvmlift3lem5  35505  cvmlift3lem6  35506  msrf  35724  elmsta  35730  mclsax  35751  mthmpps  35764  mclspps  35766  ivthALT  36517  weiunpo  36647  weiunso  36648  weiunfr  36649  weiunse  36650  poimirlem17  37958  poimirlem20  37961  ibladdnc  37998  iblabsnclem  38004  ftc1cnnclem  38012  ftc1anc  38022  ftc2nc  38023  heiborlem3  38134  iccbnd  38161  rngohom1  38289  idl0cl  38339  maxidlnr  38363  lshpne  39428  opococ  39641  opexmid  39653  hlclat  39804  lclkrslem2  41984  fzne2d  42419  dvrelog2  42503  dvrelog3  42504  0nonelalab  42506  aks4d1p1p5  42514  primrootsunit1  42536  primrootscoprmpow  42538  primrootscoprbij  42541  primrootspoweq0  42545  aks6d1c2lem3  42565  aks6d1c2  42569  aks6d1c6lem5  42616  aks5lem1  42625  aks5lem2  42626  aks5lem3a  42628  aks5lem5a  42630  unitscyglem1  42634  flt4lem5f  43090  flt4lem7  43092  nna4b4nsq  43093  gneispacern2  44566  cvgdvgrat  44740  iccshift  45948  iccsuble  45949  icoiccdif  45954  mullimc  46046  limccog  46050  mullimcf  46053  lptioo2  46061  limcmptdm  46063  limcicciooub  46065  xlimmnfvlem1  46260  xlimpnfvlem1  46264  icccncfext  46315  cncfioobdlem  46324  ditgeqiooicc  46388  itgsubsticc  46404  iblcncfioo  46406  itgiccshift  46408  itgperiod  46409  itgsbtaddcnst  46410  stoweidlem31  46459  stoweidlem36  46464  stoweidlem38  46466  stoweidlem44  46472  stoweidlem62  46490  dirkercncflem1  46531  dirkercncflem4  46534  fourierdlem26  46561  fourierdlem32  46567  fourierdlem33  46568  fourierdlem37  46572  fourierdlem42  46577  fourierdlem54  46588  fourierdlem63  46597  fourierdlem64  46598  fourierdlem65  46599  fourierdlem69  46603  fourierdlem74  46608  fourierdlem75  46609  fourierdlem79  46613  fourierdlem81  46615  fourierdlem82  46616  fourierdlem89  46623  fourierdlem90  46624  fourierdlem91  46625  fourierdlem93  46627  fourierdlem101  46635  fourierdlem111  46645  saldifcl  46747  unisalgen2  46782  hoidmv1lelem3  47021  smff  47160  sigardiv  47289  sigarcol  47292  sharhght  47293  sigaradd  47294  cevathlem1  47295  cevathlem2  47296  cevath  47297  proththd  48071  perfectALTVlem2  48192  gpgnbgrvtx0  48544  gpgnbgrvtx1  48545  imasubc2  49621  imaf1co  49624  idfullsubc  49630  fucofulem1  49779