Theorem simp2d 1161

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

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  simp2bi  1164  f1dom3fv3dif  7295  f1dom3el3dif  7296  f1prex  7315  oeeui  8639  resixp  8989  domssex  9185  cantnflem1a  9713  cantnflem1d  9716  cantnflem3  9719  cantnflem4  9720  fpwwe2lem6  10748  canthnumlem  10760  canthp1lem2  10765  wun0  10830  lelttrdi  11499  supmullem2  12315  supmul  12316  ixxdisj  13518  ixxun  13519  ixxss1  13521  ixxss2  13522  ixxss12  13523  ixxub  13524  ixxlb  13525  ubioo  13535  elicore  13556  iccgelb  13560  iccss2  13575  icodisj  13634  xov1plusxeqvd  13656  fldiv  14027  immul  15332  sqrtge0  15453  sqrtrege0  15562  icco1  15736  ruclem2  16429  ruclem3  16430  ruclem8  16434  ruclem12  16438  gcddvds  16702  crth  16984  phimullem  16985  eulerthlem1  16987  eulerthlem2  16988  prmreclem3  17125  sectcan  17959  sectco  17960  sectmon  17986  monsect  17987  funcixp  18071  funcsect  18076  invfuc  18181  coapm  18275  catciso  18315  posasymb  18522  ipodrsima  18744  pstr2  18774  psdmrn  18776  psref  18777  mhmlin  19017  subm0cl  19035  eqger  19419  eqgcpbl  19423  gaorber  19552  orbstafun  19555  cayleyth  19659  pmtrrn2  19704  pmtrfinv  19705  dfod2  19808  sylow2blem1  19864  dprdf  20252  dprdff  20258  dprdfcl  20259  dprdsplit  20294  dpjcntz  20298  ablfac1a  20315  ablfac1b  20316  lmodvsdi  21190  lbssp  21384  2idlcpblrng  21595  prmidlnr  21650  qsidomlem2  21667  evlsval3  22428  mpff  22451  mpfaddcl  22452  mpfmulcl  22453  mpfind  22454  pf1rcl  22697  mpfpf1  22699  mdetunilem2  22958  mdetunilem5  22961  mdetunilem6  22962  chfacfisfcpmat  23203  pnfnei  23568  cnptop2  23591  lmcl  23645  lmcnp  23652  flimfil  24318  tlmlmod  24538  ustbasel  24556  ustincl  24557  ustinvel  24559  ustfilxp  24562  tusunif  24617  imasdsf1olem  24722  xmeter  24782  tmsds  24833  metustexhalf  24905  nlmlmod  25027  qdensere  25118  blcvx  25147  tgqioo  25149  icccmplem2  25173  reconnlem1  25176  cnmpopc  25279  phtpcer  25346  phtpcco2  25350  pcohtpylem  25370  pcohtpy  25371  pcophtb  25380  om1addcl  25384  pi1blem  25390  pi1cpbl  25395  pi1grplem  25400  pi1inv  25403  pi1xfrf  25404  pi1xfr  25406  pi1xfrcnvlem  25407  pi1cof  25410  pi1coghm  25412  cphnlm  25523  cphsqrtcl2  25537  tcphcph  25588  lmcau  25664  bcthlem4  25678  minveclem4c  25776  minveclem2  25777  minveclem3b  25779  minveclem4  25783  minveclem6  25785  ivthicc  25809  ovolfsval  25821  ovollb2lem  25839  ovolshftlem1  25860  ovolscalem1  25864  ovolicc1  25867  ovolicc2lem2  25869  ovolicc2lem4  25871  ovolicc2lem5  25872  ovolicopnf  25875  ioombl1lem1  25909  ioombl1lem3  25911  ioombl1lem4  25912  uniioovol  25930  uniioombllem2a  25933  uniioombllem2  25934  uniioombllem3a  25935  uniioombllem3  25936  uniioombllem4  25937  uniioombllem6  25939  dyadmaxlem  25948  volivth  25958  vitalilem2  25960  vitalilem5  25963  i1frn  26028  itg2monolem1  26101  itgcnlem  26140  itgrevallem1  26145  itgreval  26147  itgle  26160  ibladd  26171  iblabslem  26178  itgspliticc  26187  itgsplitioo  26188  ditgcl  26208  ditgswap  26209  ditgsplitlem  26210  limcdif  26226  limcresi  26235  limccnp  26241  limccnp2  26242  limcco  26243  dvlip  26343  dvlip2  26345  dveq0  26350  dvgt0lem1  26352  dvivthlem1  26358  dvcnvrelem1  26367  dvcnvre  26369  dvfsumlem2  26377  ftc1lem1  26385  ftc1a  26387  ftc1lem4  26389  ftc2ditglem  26395  itgsubstlem  26398  ply1rem  26514  fta1glem1  26516  ig1pdvds  26528  plyrem  26656  facth  26657  fta1lem  26658  vieta1lem1  26663  vieta1lem2  26664  aaliou3lem3  26701  aaliou3lem4  26703  aaliou3lem7  26706  taylfvallem1  26714  tayl0  26719  taylply2  26725  radcnvle  26777  psercnlem2  26781  psercnlem1  26782  psercn  26783  pserdvlem1  26784  pserdvlem2  26785  abelth2  26799  coseq00topi  26861  coseq0negpitopi  26862  cosordlem  26888  tanord1  26895  efif1olem1  26900  loglesqrt  27119  logreclem  27120  relogbval  27130  nnlogbexp  27139  chordthmlem4  27193  quart1  27214  quartlem2  27216  quartlem3  27217  quartlem4  27218  quart  27219  acosbnd  27258  atancj  27268  atanlogsublem  27273  atantan  27281  atanbndlem  27283  dvatan  27293  atantayl  27295  rlimcnp2  27324  divsqrtsumlem  27337  ftalem5  27434  ftalem7  27436  basellem4  27441  basellem5  27442  perfectlem2  27587  dchrinv  27618  chpdifbndlem1  27910  pntibndlem2  27948  pntlemc  27952  pntlema  27953  pntlemb  27954  pntlemg  27955  pntlemh  27956  pntlemq  27958  pntlemr  27959  pntlemj  27960  pntlemi  27961  pntlemf  27962  pntlemk  27963  pntlemo  27964  pntleme  27965  pntlem3  27966  pntleml  27968  abvcxp  27972  flt4lem5f  28017  flt4lem7  28019  nna4b4nsq  28020  cutsun12  28206  lesrec  28215  eqcuts3  28220  cofcut2  28338  cofcutr  28340  cofcutrtime  28343  cutmax  28350  cutmin  28351  addsproplem4  28388  addsproplem6  28390  addsuniflem  28417  addsasslem1  28419  addsasslem2  28420  negsproplem5  28448  negsproplem6  28449  negcut2  28456  negsunif  28471  mulsproplem12  28543  sltmuls1  28563  sltmuls2  28564  mulsuniflem  28565  precsexlem11  28633  twocut  28839  pw2cut2  28878  axtgpasch  28959  cgr3simp2  29014  legso  29092  hlne2  29102  hlln  29103  mirhl  29181  inagswap  29390  inagne2  29392  dfcgrg2  29438  subumgredg2  29896  upgrres1  29924  nb3grprlem1  29991  wlkp  30227  subgrwlk  30299  spthcycl  30422  wspthsswwlkn  30537  2wlkdlem6  30550  clwwisshclwwsn  30637  erclwwlkeqlen  30640  erclwwlksym  30642  erclwwlktr  30643  clwwlkn  30647  clwwlknwrd  30655  clwwlknonex2e  30731  acycgrcycl  30783  grpoass  31135  vcsm  31194  nvf  31292  ssps  31362  minvecolem2  31507  minvecolem4c  31511  minvecolem4  31512  minvecolem5  31513  minvecolem6  31514  eigvec1  32594  inagbtwn  33078  cgrgptxfr  33083  inagcgratrgncol  33087  tgaasne  33112  eliccelico  33439  elicoelioo  33440  pmtrto1cl  33730  cyc3evpm  33781  slmdvsdi  33846  slmdvs1  33851  sdrgdvcl  33931  sdrginvcl  33932  fldgenssp  33950  imaslmod  33984  mxidlnr  34059  0ringmon1p  34159  irngnzply1lem  34392  irngnzply1  34393  ply1annig1p  34406  minplycl  34408  ply1annprmidl  34409  minplym1p  34415  minplynzm1p  34416  algextdeglem1  34419  algextdeglem2  34420  algextdeglem3  34421  algextdeglem4  34422  algextdeglem5  34423  constrsqrtcl  34481  cnre2csqlem  34612  lmxrge0  34654  sigaclci  34834  difunielsiga  34835  insiga  34840  ldsysgenld  34863  sigapildsyslem  34864  sigapildsys  34865  ldgenpisyslem1  34866  measvnul  34909  sibfrn  35039  eulerpartlemt  35073  eulerpartlemmf  35077  tg5segofs  35375  lpadleft  35385  dfk22  36013  subfacp1lem2a  36112  subfacp1lem3  36114  subfacp1lem4  36115  subfacp1lem5  36116  sconnpht2  36170  sconnpi1  36171  resconn  36178  cvmsss  36199  cvmsn0  36200  cvmlift2lem3  36237  cvmlift2lem7  36241  cvmliftphtlem  36249  cvmliftpht  36250  cvmlift3lem5  36255  cvmlift3lem6  36256  msrf  36474  elmsta  36480  mclsax  36501  mthmpps  36514  mclspps  36516  ivthALT  37301  weiunpo  37431  weiunso  37432  weiunfr  37433  weiunse  37434  poimirlem17  38747  poimirlem20  38750  ibladdnc  38787  iblabsnclem  38793  ftc1cnnclem  38801  ftc1anc  38811  ftc2nc  38812  heiborlem3  38939  iccbnd  38966  rngohom1  39094  idl0cl  39144  maxidlnr  39168  lshpne  40231  opococ  40444  opexmid  40456  hlclat  40607  lclkrslem2  42787  fzne2d  43222  dvrelog2  43306  dvrelog3  43307  0nonelalab  43309  aks4d1p1p5  43317  primrootsunit1  43339  primrootscoprmpow  43341  primrootscoprbij  43344  primrootspoweq0  43348  aks6d1c2lem3  43368  aks6d1c2  43372  aks6d1c6lem5  43419  aks5lem1  43428  aks5lem2  43429  aks5lem3a  43431  aks5lem5a  43433  unitscyglem1  43437  gneispacern2  45331  cvgdvgrat  45489  iccshift  46735  iccsuble  46736  icoiccdif  46741  mullimc  46833  limccog  46837  mullimcf  46840  lptioo2  46848  limcmptdm  46850  limcicciooub  46852  xlimmnfvlem1  47047  xlimpnfvlem1  47051  icccncfext  47102  cncfioobdlem  47111  ditgeqiooicc  47175  itgsubsticc  47191  iblcncfioo  47193  itgiccshift  47195  itgperiod  47196  itgsbtaddcnst  47197  stoweidlem31  47246  stoweidlem36  47251  stoweidlem38  47253  stoweidlem44  47259  stoweidlem62  47277  dirkercncflem1  47318  dirkercncflem4  47321  fourierdlem26  47348  fourierdlem32  47354  fourierdlem33  47355  fourierdlem37  47359  fourierdlem42  47364  fourierdlem54  47375  fourierdlem63  47384  fourierdlem64  47385  fourierdlem65  47386  fourierdlem69  47390  fourierdlem74  47395  fourierdlem75  47396  fourierdlem79  47400  fourierdlem81  47402  fourierdlem82  47403  fourierdlem89  47410  fourierdlem90  47411  fourierdlem91  47412  fourierdlem93  47414  fourierdlem101  47422  fourierdlem111  47432  saldifcl  47534  unisalgen2  47569  hoidmv1lelem3  47808  smff  47947  sigardiv  48076  sigarcol  48079  sharhght  48080  sigaradd  48081  cevathlem1  48082  cevathlem2  48083  cevath  48084  proththd  48904  perfectALTVlem2  49025  gpgnbgrvtx0  49377  gpgnbgrvtx1  49378  imasubc2  50473  imaf1co  50476  idfullsubc  50482  fucofulem1  50637  parcatid2  50968  parcatid  50969  rr3fv2cld  51228