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  7209  f1dom3el3dif  7210  f1prex  7225  oeeui  8527  resixp  8867  domssex  9062  cantnflem1a  9600  cantnflem1d  9603  cantnflem3  9606  cantnflem4  9607  fpwwe2lem6  10549  canthnumlem  10561  canthp1lem2  10566  wun0  10631  lelttrdi  11296  supmullem2  12114  supmul  12115  ixxdisj  13281  ixxun  13282  ixxss1  13284  ixxss2  13285  ixxss12  13286  ixxub  13287  ixxlb  13288  ubioo  13298  elicore  13319  iccgelb  13323  iccss2  13338  icodisj  13397  xov1plusxeqvd  13419  fldiv  13782  immul  15061  sqrtge0  15182  sqrtrege0  15291  icco1  15465  ruclem2  16159  ruclem3  16160  ruclem8  16164  ruclem12  16168  gcddvds  16432  crth  16707  phimullem  16708  eulerthlem1  16710  eulerthlem2  16711  prmreclem3  16848  sectcan  17680  sectco  17681  sectmon  17707  monsect  17708  funcixp  17792  funcsect  17797  invfuc  17902  coapm  17996  catciso  18036  posasymb  18243  ipodrsima  18465  pstr2  18495  psdmrn  18497  psref  18498  mhmlin  18685  subm0cl  18703  eqger  19075  eqgcpbl  19079  gaorber  19205  orbstafun  19208  cayleyth  19312  pmtrrn2  19357  pmtrfinv  19358  dfod2  19461  sylow2blem1  19517  dprdf  19905  dprdff  19911  dprdfcl  19912  dprdsplit  19947  dpjcntz  19951  ablfac1a  19968  ablfac1b  19969  lmodvsdi  20806  lbssp  21001  2idlcpblrng  21196  mpff  22027  mpfaddcl  22028  mpfmulcl  22029  mpfind  22030  pf1rcl  22252  mpfpf1  22254  mdetunilem2  22516  mdetunilem5  22519  mdetunilem6  22520  chfacfisfcpmat  22758  pnfnei  23123  cnptop2  23146  lmcl  23200  lmcnp  23207  flimfil  23872  tlmlmod  24092  ustbasel  24110  ustincl  24111  ustinvel  24113  ustfilxp  24116  tusunif  24172  imasdsf1olem  24277  xmeter  24337  tmsds  24388  metustexhalf  24460  nlmlmod  24582  qdensere  24673  blcvx  24702  tgqioo  24704  icccmplem2  24728  reconnlem1  24731  cnmpopc  24838  phtpcer  24910  phtpcco2  24915  pcohtpylem  24935  pcohtpy  24936  pcophtb  24945  om1addcl  24949  pi1blem  24955  pi1cpbl  24960  pi1grplem  24965  pi1inv  24968  pi1xfrf  24969  pi1xfr  24971  pi1xfrcnvlem  24972  pi1cof  24975  pi1coghm  24977  cphnlm  25088  cphsqrtcl2  25102  tcphcph  25153  lmcau  25229  bcthlem4  25243  minveclem4c  25341  minveclem2  25342  minveclem3b  25344  minveclem4  25348  minveclem6  25350  ivthicc  25375  ovolfsval  25387  ovollb2lem  25405  ovolshftlem1  25426  ovolscalem1  25430  ovolicc1  25433  ovolicc2lem2  25435  ovolicc2lem4  25437  ovolicc2lem5  25438  ovolicopnf  25441  ioombl1lem1  25475  ioombl1lem3  25477  ioombl1lem4  25478  uniioovol  25496  uniioombllem2a  25499  uniioombllem2  25500  uniioombllem3a  25501  uniioombllem3  25502  uniioombllem4  25503  uniioombllem6  25505  dyadmaxlem  25514  volivth  25524  vitalilem2  25526  vitalilem5  25529  i1frn  25594  itg2monolem1  25667  itgcnlem  25707  itgrevallem1  25712  itgreval  25714  itgle  25727  ibladd  25738  iblabslem  25745  itgspliticc  25754  itgsplitioo  25755  ditgcl  25775  ditgswap  25776  ditgsplitlem  25777  limcdif  25793  limcresi  25802  limccnp  25808  limccnp2  25809  limcco  25810  dvlip  25914  dvlip2  25916  dveq0  25921  dvgt0lem1  25923  dvivthlem1  25929  dvcnvrelem1  25938  dvcnvre  25940  dvfsumlem2  25949  dvfsumlem2OLD  25950  ftc1lem1  25958  ftc1a  25960  ftc1lem4  25962  ftc2ditglem  25968  itgsubstlem  25971  ply1rem  26087  fta1glem1  26089  ig1pdvds  26101  plyrem  26229  facth  26230  fta1lem  26231  vieta1lem1  26234  vieta1lem2  26235  aaliou3lem3  26268  aaliou3lem4  26270  aaliou3lem7  26273  taylfvallem1  26280  tayl0  26285  taylply2  26291  taylply2OLD  26292  radcnvle  26345  psercnlem2  26350  psercnlem1  26351  psercn  26352  pserdvlem1  26353  pserdvlem2  26354  abelth2  26368  coseq00topi  26427  coseq0negpitopi  26428  cosordlem  26455  tanord1  26462  efif1olem1  26467  loglesqrt  26687  logreclem  26688  relogbval  26698  nnlogbexp  26707  chordthmlem4  26761  quart1  26782  quartlem2  26784  quartlem3  26785  quartlem4  26786  quart  26787  acosbnd  26826  atancj  26836  atanlogsublem  26841  atantan  26849  atanbndlem  26851  dvatan  26861  atantayl  26863  rlimcnp2  26892  divsqrtsumlem  26906  ftalem5  27003  ftalem7  27005  basellem4  27010  basellem5  27011  perfectlem2  27157  dchrinv  27188  chpdifbndlem1  27480  pntibndlem2  27518  pntlemc  27522  pntlema  27523  pntlemb  27524  pntlemg  27525  pntlemh  27526  pntlemq  27528  pntlemr  27529  pntlemj  27530  pntlemi  27531  pntlemf  27532  pntlemk  27533  pntlemo  27534  pntleme  27535  pntlem3  27536  pntleml  27538  abvcxp  27542  scutun12  27739  slerec  27748  eqscut3  27753  cofcut2  27853  cofcutr  27855  cofcutrtime  27858  cutmax  27865  cutmin  27866  addsproplem4  27902  addsproplem6  27904  addsuniflem  27931  addsasslem1  27933  addsasslem2  27934  negsproplem5  27961  negsproplem6  27962  negscut2  27969  negsunif  27984  mulsproplem12  28053  ssltmul1  28073  ssltmul2  28074  mulsuniflem  28075  precsexlem11  28142  twocut  28333  axtgpasch  28430  cgr3simp2  28484  legso  28562  hlne2  28569  hlln  28570  mirhl  28642  inagswap  28804  inagne2  28806  dfcgrg2  28826  subumgredg2  29248  upgrres1  29276  nb3grprlem1  29343  wlkp  29580  wspthsswwlkn  29881  2wlkdlem6  29894  clwwisshclwwsn  29978  erclwwlkeqlen  29981  erclwwlksym  29983  erclwwlktr  29984  clwwlkn  29988  clwwlknwrd  29996  clwwlknonex2e  30072  grpoass  30465  vcsm  30524  nvf  30622  ssps  30692  minvecolem2  30837  minvecolem4c  30841  minvecolem4  30842  minvecolem5  30843  minvecolem6  30844  eigvec1  31924  eliccelico  32733  elicoelioo  32734  pmtrto1cl  33054  cyc3evpm  33105  slmdvsdi  33167  slmdvs1  33172  sdrgdvcl  33248  sdrginvcl  33249  fldgenssp  33267  imaslmod  33300  prmidlnr  33386  qsidomlem2  33400  mxidlnr  33411  0ringmon1p  33502  irngnzply1lem  33661  irngnzply1  33662  ply1annig1p  33670  minplycl  33672  ply1annprmidl  33673  minplym1p  33679  minplynzm1p  33680  algextdeglem1  33683  algextdeglem2  33684  algextdeglem3  33685  algextdeglem4  33686  algextdeglem5  33687  constrsqrtcl  33745  cnre2csqlem  33876  lmxrge0  33918  sigaclci  34098  difelsiga  34099  insiga  34103  ldsysgenld  34126  sigapildsyslem  34127  sigapildsys  34128  ldgenpisyslem1  34129  measvnul  34172  sibfrn  34304  eulerpartlemt  34338  eulerpartlemmf  34342  tg5segofs  34640  lpadleft  34650  spthcycl  35101  subgrwlk  35104  acycgrcycl  35119  subfacp1lem2a  35152  subfacp1lem3  35154  subfacp1lem4  35155  subfacp1lem5  35156  sconnpht2  35210  sconnpi1  35211  resconn  35218  cvmsss  35239  cvmsn0  35240  cvmlift2lem3  35277  cvmlift2lem7  35281  cvmliftphtlem  35289  cvmliftpht  35290  cvmlift3lem5  35295  cvmlift3lem6  35296  msrf  35514  elmsta  35520  mclsax  35541  mthmpps  35554  mclspps  35556  ivthALT  36308  weiunpo  36438  weiunso  36439  weiunfr  36440  weiunse  36441  poimirlem17  37616  poimirlem20  37619  ibladdnc  37656  iblabsnclem  37662  ftc1cnnclem  37670  ftc1anc  37680  ftc2nc  37681  heiborlem3  37792  iccbnd  37819  rngohom1  37947  idl0cl  37997  maxidlnr  38021  lshpne  38960  opococ  39173  opexmid  39185  hlclat  39336  lclkrslem2  41517  fzne2d  41953  dvrelog2  42037  dvrelog3  42038  0nonelalab  42040  aks4d1p1p5  42048  primrootsunit1  42070  primrootscoprmpow  42072  primrootscoprbij  42075  primrootspoweq0  42079  aks6d1c2lem3  42099  aks6d1c2  42103  aks6d1c6lem5  42150  aks5lem1  42159  aks5lem2  42160  aks5lem3a  42162  aks5lem5a  42164  unitscyglem1  42168  evlsval3  42532  flt4lem5f  42630  flt4lem7  42632  nna4b4nsq  42633  gneispacern2  44112  cvgdvgrat  44286  iccshift  45500  iccsuble  45501  icoiccdif  45506  mullimc  45598  limccog  45602  mullimcf  45605  lptioo2  45613  limcmptdm  45617  limcicciooub  45619  xlimmnfvlem1  45814  xlimpnfvlem1  45818  icccncfext  45869  cncfioobdlem  45878  ditgeqiooicc  45942  itgsubsticc  45958  iblcncfioo  45960  itgiccshift  45962  itgperiod  45963  itgsbtaddcnst  45964  stoweidlem31  46013  stoweidlem36  46018  stoweidlem38  46020  stoweidlem44  46026  stoweidlem62  46044  dirkercncflem1  46085  dirkercncflem4  46088  fourierdlem26  46115  fourierdlem32  46121  fourierdlem33  46122  fourierdlem37  46126  fourierdlem42  46131  fourierdlem54  46142  fourierdlem63  46151  fourierdlem64  46152  fourierdlem65  46153  fourierdlem69  46157  fourierdlem74  46162  fourierdlem75  46163  fourierdlem79  46167  fourierdlem81  46169  fourierdlem82  46170  fourierdlem89  46177  fourierdlem90  46178  fourierdlem91  46179  fourierdlem93  46181  fourierdlem101  46189  fourierdlem111  46199  saldifcl  46301  unisalgen2  46336  hoidmv1lelem3  46575  smff  46714  sigardiv  46843  sigarcol  46846  sharhght  46847  sigaradd  46848  cevathlem1  46849  cevathlem2  46850  cevath  46851  proththd  47599  perfectALTVlem2  47707  gpgnbgrvtx0  48049  gpgnbgrvtx1  48050  imasubc2  49125  imaf1co  49128  idfullsubc  49134  fucofulem1  49283