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  7216  f1dom3el3dif  7217  f1prex  7232  oeeui  8532  resixp  8875  domssex  9070  cantnflem1a  9598  cantnflem1d  9601  cantnflem3  9604  cantnflem4  9605  fpwwe2lem6  10551  canthnumlem  10563  canthp1lem2  10568  wun0  10633  lelttrdi  11299  supmullem2  12117  supmul  12118  ixxdisj  13280  ixxun  13281  ixxss1  13283  ixxss2  13284  ixxss12  13285  ixxub  13286  ixxlb  13287  ubioo  13297  elicore  13318  iccgelb  13322  iccss2  13337  icodisj  13396  xov1plusxeqvd  13418  fldiv  13784  immul  15063  sqrtge0  15184  sqrtrege0  15293  icco1  15467  ruclem2  16161  ruclem3  16162  ruclem8  16166  ruclem12  16170  gcddvds  16434  crth  16709  phimullem  16710  eulerthlem1  16712  eulerthlem2  16713  prmreclem3  16850  sectcan  17683  sectco  17684  sectmon  17710  monsect  17711  funcixp  17795  funcsect  17800  invfuc  17905  coapm  17999  catciso  18039  posasymb  18246  ipodrsima  18468  pstr2  18498  psdmrn  18500  psref  18501  mhmlin  18722  subm0cl  18740  eqger  19111  eqgcpbl  19115  gaorber  19241  orbstafun  19244  cayleyth  19348  pmtrrn2  19393  pmtrfinv  19394  dfod2  19497  sylow2blem1  19553  dprdf  19941  dprdff  19947  dprdfcl  19948  dprdsplit  19983  dpjcntz  19987  ablfac1a  20004  ablfac1b  20005  lmodvsdi  20840  lbssp  21035  2idlcpblrng  21230  evlsval3  22048  mpff  22071  mpfaddcl  22072  mpfmulcl  22073  mpfind  22074  pf1rcl  22297  mpfpf1  22299  mdetunilem2  22561  mdetunilem5  22564  mdetunilem6  22565  chfacfisfcpmat  22803  pnfnei  23168  cnptop2  23191  lmcl  23245  lmcnp  23252  flimfil  23917  tlmlmod  24137  ustbasel  24155  ustincl  24156  ustinvel  24158  ustfilxp  24161  tusunif  24216  imasdsf1olem  24321  xmeter  24381  tmsds  24432  metustexhalf  24504  nlmlmod  24626  qdensere  24717  blcvx  24746  tgqioo  24748  icccmplem2  24772  reconnlem1  24775  cnmpopc  24882  phtpcer  24954  phtpcco2  24959  pcohtpylem  24979  pcohtpy  24980  pcophtb  24989  om1addcl  24993  pi1blem  24999  pi1cpbl  25004  pi1grplem  25009  pi1inv  25012  pi1xfrf  25013  pi1xfr  25015  pi1xfrcnvlem  25016  pi1cof  25019  pi1coghm  25021  cphnlm  25132  cphsqrtcl2  25146  tcphcph  25197  lmcau  25273  bcthlem4  25287  minveclem4c  25385  minveclem2  25386  minveclem3b  25388  minveclem4  25392  minveclem6  25394  ivthicc  25419  ovolfsval  25431  ovollb2lem  25449  ovolshftlem1  25470  ovolscalem1  25474  ovolicc1  25477  ovolicc2lem2  25479  ovolicc2lem4  25481  ovolicc2lem5  25482  ovolicopnf  25485  ioombl1lem1  25519  ioombl1lem3  25521  ioombl1lem4  25522  uniioovol  25540  uniioombllem2a  25543  uniioombllem2  25544  uniioombllem3a  25545  uniioombllem3  25546  uniioombllem4  25547  uniioombllem6  25549  dyadmaxlem  25558  volivth  25568  vitalilem2  25570  vitalilem5  25573  i1frn  25638  itg2monolem1  25711  itgcnlem  25751  itgrevallem1  25756  itgreval  25758  itgle  25771  ibladd  25782  iblabslem  25789  itgspliticc  25798  itgsplitioo  25799  ditgcl  25819  ditgswap  25820  ditgsplitlem  25821  limcdif  25837  limcresi  25846  limccnp  25852  limccnp2  25853  limcco  25854  dvlip  25958  dvlip2  25960  dveq0  25965  dvgt0lem1  25967  dvivthlem1  25973  dvcnvrelem1  25982  dvcnvre  25984  dvfsumlem2  25993  dvfsumlem2OLD  25994  ftc1lem1  26002  ftc1a  26004  ftc1lem4  26006  ftc2ditglem  26012  itgsubstlem  26015  ply1rem  26131  fta1glem1  26133  ig1pdvds  26145  plyrem  26273  facth  26274  fta1lem  26275  vieta1lem1  26278  vieta1lem2  26279  aaliou3lem3  26312  aaliou3lem4  26314  aaliou3lem7  26317  taylfvallem1  26324  tayl0  26329  taylply2  26335  taylply2OLD  26336  radcnvle  26389  psercnlem2  26394  psercnlem1  26395  psercn  26396  pserdvlem1  26397  pserdvlem2  26398  abelth2  26412  coseq00topi  26471  coseq0negpitopi  26472  cosordlem  26499  tanord1  26506  efif1olem1  26511  loglesqrt  26731  logreclem  26732  relogbval  26742  nnlogbexp  26751  chordthmlem4  26805  quart1  26826  quartlem2  26828  quartlem3  26829  quartlem4  26830  quart  26831  acosbnd  26870  atancj  26880  atanlogsublem  26885  atantan  26893  atanbndlem  26895  dvatan  26905  atantayl  26907  rlimcnp2  26936  divsqrtsumlem  26950  ftalem5  27047  ftalem7  27049  basellem4  27054  basellem5  27055  perfectlem2  27201  dchrinv  27232  chpdifbndlem1  27524  pntibndlem2  27562  pntlemc  27566  pntlema  27567  pntlemb  27568  pntlemg  27569  pntlemh  27570  pntlemq  27572  pntlemr  27573  pntlemj  27574  pntlemi  27575  pntlemf  27576  pntlemk  27577  pntlemo  27578  pntleme  27579  pntlem3  27580  pntleml  27582  abvcxp  27586  scutun12  27788  slerec  27797  eqscut3  27802  cofcut2  27904  cofcutr  27906  cofcutrtime  27909  cutmax  27916  cutmin  27917  addsproplem4  27954  addsproplem6  27956  addsuniflem  27983  addsasslem1  27985  addsasslem2  27986  negsproplem5  28014  negsproplem6  28015  negscut2  28022  negsunif  28037  mulsproplem12  28109  ssltmul1  28129  ssltmul2  28130  mulsuniflem  28131  precsexlem11  28198  twocut  28402  pw2cut2  28441  axtgpasch  28522  cgr3simp2  28576  legso  28654  hlne2  28661  hlln  28662  mirhl  28734  inagswap  28896  inagne2  28898  dfcgrg2  28918  subumgredg2  29341  upgrres1  29369  nb3grprlem1  29436  wlkp  29673  wspthsswwlkn  29974  2wlkdlem6  29987  clwwisshclwwsn  30074  erclwwlkeqlen  30077  erclwwlksym  30079  erclwwlktr  30080  clwwlkn  30084  clwwlknwrd  30092  clwwlknonex2e  30168  grpoass  30561  vcsm  30620  nvf  30718  ssps  30788  minvecolem2  30933  minvecolem4c  30937  minvecolem4  30938  minvecolem5  30939  minvecolem6  30940  eigvec1  32020  eliccelico  32838  elicoelioo  32839  pmtrto1cl  33162  cyc3evpm  33213  slmdvsdi  33278  slmdvs1  33283  sdrgdvcl  33362  sdrginvcl  33363  fldgenssp  33381  imaslmod  33415  prmidlnr  33501  qsidomlem2  33515  mxidlnr  33526  0ringmon1p  33619  irngnzply1lem  33828  irngnzply1  33829  ply1annig1p  33842  minplycl  33844  ply1annprmidl  33845  minplym1p  33851  minplynzm1p  33852  algextdeglem1  33855  algextdeglem2  33856  algextdeglem3  33857  algextdeglem4  33858  algextdeglem5  33859  constrsqrtcl  33917  cnre2csqlem  34048  lmxrge0  34090  sigaclci  34270  difelsiga  34271  insiga  34275  ldsysgenld  34298  sigapildsyslem  34299  sigapildsys  34300  ldgenpisyslem1  34301  measvnul  34344  sibfrn  34475  eulerpartlemt  34509  eulerpartlemmf  34513  tg5segofs  34811  lpadleft  34821  spthcycl  35304  subgrwlk  35307  acycgrcycl  35322  subfacp1lem2a  35355  subfacp1lem3  35357  subfacp1lem4  35358  subfacp1lem5  35359  sconnpht2  35413  sconnpi1  35414  resconn  35421  cvmsss  35442  cvmsn0  35443  cvmlift2lem3  35480  cvmlift2lem7  35484  cvmliftphtlem  35492  cvmliftpht  35493  cvmlift3lem5  35498  cvmlift3lem6  35499  msrf  35717  elmsta  35723  mclsax  35744  mthmpps  35757  mclspps  35759  ivthALT  36510  weiunpo  36640  weiunso  36641  weiunfr  36642  weiunse  36643  poimirlem17  37809  poimirlem20  37812  ibladdnc  37849  iblabsnclem  37855  ftc1cnnclem  37863  ftc1anc  37873  ftc2nc  37874  heiborlem3  37985  iccbnd  38012  rngohom1  38140  idl0cl  38190  maxidlnr  38214  lshpne  39279  opococ  39492  opexmid  39504  hlclat  39655  lclkrslem2  41835  fzne2d  42271  dvrelog2  42355  dvrelog3  42356  0nonelalab  42358  aks4d1p1p5  42366  primrootsunit1  42388  primrootscoprmpow  42390  primrootscoprbij  42393  primrootspoweq0  42397  aks6d1c2lem3  42417  aks6d1c2  42421  aks6d1c6lem5  42468  aks5lem1  42477  aks5lem2  42478  aks5lem3a  42480  aks5lem5a  42482  unitscyglem1  42486  flt4lem5f  42936  flt4lem7  42938  nna4b4nsq  42939  gneispacern2  44416  cvgdvgrat  44590  iccshift  45800  iccsuble  45801  icoiccdif  45806  mullimc  45898  limccog  45902  mullimcf  45905  lptioo2  45913  limcmptdm  45915  limcicciooub  45917  xlimmnfvlem1  46112  xlimpnfvlem1  46116  icccncfext  46167  cncfioobdlem  46176  ditgeqiooicc  46240  itgsubsticc  46256  iblcncfioo  46258  itgiccshift  46260  itgperiod  46261  itgsbtaddcnst  46262  stoweidlem31  46311  stoweidlem36  46316  stoweidlem38  46318  stoweidlem44  46324  stoweidlem62  46342  dirkercncflem1  46383  dirkercncflem4  46386  fourierdlem26  46413  fourierdlem32  46419  fourierdlem33  46420  fourierdlem37  46424  fourierdlem42  46429  fourierdlem54  46440  fourierdlem63  46449  fourierdlem64  46450  fourierdlem65  46451  fourierdlem69  46455  fourierdlem74  46460  fourierdlem75  46461  fourierdlem79  46465  fourierdlem81  46467  fourierdlem82  46468  fourierdlem89  46475  fourierdlem90  46476  fourierdlem91  46477  fourierdlem93  46479  fourierdlem101  46487  fourierdlem111  46497  saldifcl  46599  unisalgen2  46634  hoidmv1lelem3  46873  smff  47012  sigardiv  47141  sigarcol  47144  sharhght  47145  sigaradd  47146  cevathlem1  47147  cevathlem2  47148  cevath  47149  proththd  47896  perfectALTVlem2  48004  gpgnbgrvtx0  48356  gpgnbgrvtx1  48357  imasubc2  49433  imaf1co  49436  idfullsubc  49442  fucofulem1  49591