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  7214  f1dom3el3dif  7215  f1prex  7230  oeeui  8529  resixp  8872  domssex  9067  cantnflem1a  9595  cantnflem1d  9598  cantnflem3  9601  cantnflem4  9602  fpwwe2lem6  10548  canthnumlem  10560  canthp1lem2  10565  wun0  10630  lelttrdi  11297  supmullem2  12116  supmul  12117  ixxdisj  13302  ixxun  13303  ixxss1  13305  ixxss2  13306  ixxss12  13307  ixxub  13308  ixxlb  13309  ubioo  13319  elicore  13340  iccgelb  13344  iccss2  13359  icodisj  13418  xov1plusxeqvd  13440  fldiv  13808  immul  15087  sqrtge0  15208  sqrtrege0  15317  icco1  15491  ruclem2  16188  ruclem3  16189  ruclem8  16193  ruclem12  16197  gcddvds  16461  crth  16737  phimullem  16738  eulerthlem1  16740  eulerthlem2  16741  prmreclem3  16878  sectcan  17711  sectco  17712  sectmon  17738  monsect  17739  funcixp  17823  funcsect  17828  invfuc  17933  coapm  18027  catciso  18067  posasymb  18274  ipodrsima  18496  pstr2  18526  psdmrn  18528  psref  18529  mhmlin  18750  subm0cl  18768  eqger  19142  eqgcpbl  19146  gaorber  19272  orbstafun  19275  cayleyth  19379  pmtrrn2  19424  pmtrfinv  19425  dfod2  19528  sylow2blem1  19584  dprdf  19972  dprdff  19978  dprdfcl  19979  dprdsplit  20014  dpjcntz  20018  ablfac1a  20035  ablfac1b  20036  lmodvsdi  20869  lbssp  21064  2idlcpblrng  21259  evlsval3  22076  mpff  22099  mpfaddcl  22100  mpfmulcl  22101  mpfind  22102  pf1rcl  22323  mpfpf1  22325  mdetunilem2  22587  mdetunilem5  22590  mdetunilem6  22591  chfacfisfcpmat  22829  pnfnei  23194  cnptop2  23217  lmcl  23271  lmcnp  23278  flimfil  23943  tlmlmod  24163  ustbasel  24181  ustincl  24182  ustinvel  24184  ustfilxp  24187  tusunif  24242  imasdsf1olem  24347  xmeter  24407  tmsds  24458  metustexhalf  24530  nlmlmod  24652  qdensere  24743  blcvx  24772  tgqioo  24774  icccmplem2  24798  reconnlem1  24801  cnmpopc  24904  phtpcer  24971  phtpcco2  24975  pcohtpylem  24995  pcohtpy  24996  pcophtb  25005  om1addcl  25009  pi1blem  25015  pi1cpbl  25020  pi1grplem  25025  pi1inv  25028  pi1xfrf  25029  pi1xfr  25031  pi1xfrcnvlem  25032  pi1cof  25035  pi1coghm  25037  cphnlm  25148  cphsqrtcl2  25162  tcphcph  25213  lmcau  25289  bcthlem4  25303  minveclem4c  25401  minveclem2  25402  minveclem3b  25404  minveclem4  25408  minveclem6  25410  ivthicc  25434  ovolfsval  25446  ovollb2lem  25464  ovolshftlem1  25485  ovolscalem1  25489  ovolicc1  25492  ovolicc2lem2  25494  ovolicc2lem4  25496  ovolicc2lem5  25497  ovolicopnf  25500  ioombl1lem1  25534  ioombl1lem3  25536  ioombl1lem4  25537  uniioovol  25555  uniioombllem2a  25558  uniioombllem2  25559  uniioombllem3a  25560  uniioombllem3  25561  uniioombllem4  25562  uniioombllem6  25564  dyadmaxlem  25573  volivth  25583  vitalilem2  25585  vitalilem5  25588  i1frn  25653  itg2monolem1  25726  itgcnlem  25766  itgrevallem1  25771  itgreval  25773  itgle  25786  ibladd  25797  iblabslem  25804  itgspliticc  25813  itgsplitioo  25814  ditgcl  25834  ditgswap  25835  ditgsplitlem  25836  limcdif  25852  limcresi  25861  limccnp  25867  limccnp2  25868  limcco  25869  dvlip  25970  dvlip2  25972  dveq0  25977  dvgt0lem1  25979  dvivthlem1  25985  dvcnvrelem1  25994  dvcnvre  25996  dvfsumlem2  26005  dvfsumlem2OLD  26006  ftc1lem1  26014  ftc1a  26016  ftc1lem4  26018  ftc2ditglem  26024  itgsubstlem  26027  ply1rem  26143  fta1glem1  26145  ig1pdvds  26157  plyrem  26284  facth  26285  fta1lem  26286  vieta1lem1  26289  vieta1lem2  26290  aaliou3lem3  26323  aaliou3lem4  26325  aaliou3lem7  26328  taylfvallem1  26335  tayl0  26340  taylply2  26346  taylply2OLD  26347  radcnvle  26400  psercnlem2  26405  psercnlem1  26406  psercn  26407  pserdvlem1  26408  pserdvlem2  26409  abelth2  26423  coseq00topi  26482  coseq0negpitopi  26483  cosordlem  26510  tanord1  26517  efif1olem1  26522  loglesqrt  26742  logreclem  26743  relogbval  26753  nnlogbexp  26762  chordthmlem4  26816  quart1  26837  quartlem2  26839  quartlem3  26840  quartlem4  26841  quart  26842  acosbnd  26881  atancj  26891  atanlogsublem  26896  atantan  26904  atanbndlem  26906  dvatan  26916  atantayl  26918  rlimcnp2  26947  divsqrtsumlem  26961  ftalem5  27058  ftalem7  27060  basellem4  27065  basellem5  27066  perfectlem2  27212  dchrinv  27243  chpdifbndlem1  27535  pntibndlem2  27573  pntlemc  27577  pntlema  27578  pntlemb  27579  pntlemg  27580  pntlemh  27581  pntlemq  27583  pntlemr  27584  pntlemj  27585  pntlemi  27586  pntlemf  27587  pntlemk  27588  pntlemo  27589  pntleme  27590  pntlem3  27591  pntleml  27593  abvcxp  27597  cutsun12  27801  lesrec  27810  eqcuts3  27815  cofcut2  27933  cofcutr  27935  cofcutrtime  27938  cutmax  27945  cutmin  27946  addsproplem4  27983  addsproplem6  27985  addsuniflem  28012  addsasslem1  28014  addsasslem2  28015  negsproplem5  28043  negsproplem6  28044  negcut2  28051  negsunif  28066  mulsproplem12  28138  sltmuls1  28158  sltmuls2  28159  mulsuniflem  28160  precsexlem11  28228  twocut  28434  pw2cut2  28473  axtgpasch  28554  cgr3simp2  28608  legso  28686  hlne2  28693  hlln  28694  mirhl  28766  inagswap  28928  inagne2  28930  dfcgrg2  28950  subumgredg2  29373  upgrres1  29401  nb3grprlem1  29468  wlkp  29705  wspthsswwlkn  30006  2wlkdlem6  30019  clwwisshclwwsn  30106  erclwwlkeqlen  30109  erclwwlksym  30111  erclwwlktr  30112  clwwlkn  30116  clwwlknwrd  30124  clwwlknonex2e  30200  grpoass  30594  vcsm  30653  nvf  30751  ssps  30821  minvecolem2  30966  minvecolem4c  30970  minvecolem4  30971  minvecolem5  30972  minvecolem6  30973  eigvec1  32053  eliccelico  32870  elicoelioo  32871  pmtrto1cl  33180  cyc3evpm  33231  slmdvsdi  33296  slmdvs1  33301  sdrgdvcl  33380  sdrginvcl  33381  fldgenssp  33399  imaslmod  33433  prmidlnr  33519  qsidomlem2  33533  mxidlnr  33544  0ringmon1p  33637  irngnzply1lem  33855  irngnzply1  33856  ply1annig1p  33869  minplycl  33871  ply1annprmidl  33872  minplym1p  33878  minplynzm1p  33879  algextdeglem1  33882  algextdeglem2  33883  algextdeglem3  33884  algextdeglem4  33885  algextdeglem5  33886  constrsqrtcl  33944  cnre2csqlem  34075  lmxrge0  34117  sigaclci  34297  difelsiga  34298  insiga  34302  ldsysgenld  34325  sigapildsyslem  34326  sigapildsys  34327  ldgenpisyslem1  34328  measvnul  34371  sibfrn  34502  eulerpartlemt  34536  eulerpartlemmf  34540  tg5segofs  34838  lpadleft  34848  spthcycl  35332  subgrwlk  35335  acycgrcycl  35350  subfacp1lem2a  35383  subfacp1lem3  35385  subfacp1lem4  35386  subfacp1lem5  35387  sconnpht2  35441  sconnpi1  35442  resconn  35449  cvmsss  35470  cvmsn0  35471  cvmlift2lem3  35508  cvmlift2lem7  35512  cvmliftphtlem  35520  cvmliftpht  35521  cvmlift3lem5  35526  cvmlift3lem6  35527  msrf  35745  elmsta  35751  mclsax  35772  mthmpps  35785  mclspps  35787  ivthALT  36538  weiunpo  36668  weiunso  36669  weiunfr  36670  weiunse  36671  poimirlem17  37969  poimirlem20  37972  ibladdnc  38009  iblabsnclem  38015  ftc1cnnclem  38023  ftc1anc  38033  ftc2nc  38034  heiborlem3  38145  iccbnd  38172  rngohom1  38300  idl0cl  38350  maxidlnr  38374  lshpne  39439  opococ  39652  opexmid  39664  hlclat  39815  lclkrslem2  41995  fzne2d  42430  dvrelog2  42514  dvrelog3  42515  0nonelalab  42517  aks4d1p1p5  42525  primrootsunit1  42547  primrootscoprmpow  42549  primrootscoprbij  42552  primrootspoweq0  42556  aks6d1c2lem3  42576  aks6d1c2  42580  aks6d1c6lem5  42627  aks5lem1  42636  aks5lem2  42637  aks5lem3a  42639  aks5lem5a  42641  unitscyglem1  42645  flt4lem5f  43101  flt4lem7  43103  nna4b4nsq  43104  gneispacern2  44581  cvgdvgrat  44755  iccshift  45963  iccsuble  45964  icoiccdif  45969  mullimc  46061  limccog  46065  mullimcf  46068  lptioo2  46076  limcmptdm  46078  limcicciooub  46080  xlimmnfvlem1  46275  xlimpnfvlem1  46279  icccncfext  46330  cncfioobdlem  46339  ditgeqiooicc  46403  itgsubsticc  46419  iblcncfioo  46421  itgiccshift  46423  itgperiod  46424  itgsbtaddcnst  46425  stoweidlem31  46474  stoweidlem36  46479  stoweidlem38  46481  stoweidlem44  46487  stoweidlem62  46505  dirkercncflem1  46546  dirkercncflem4  46549  fourierdlem26  46576  fourierdlem32  46582  fourierdlem33  46583  fourierdlem37  46587  fourierdlem42  46592  fourierdlem54  46603  fourierdlem63  46612  fourierdlem64  46613  fourierdlem65  46614  fourierdlem69  46618  fourierdlem74  46623  fourierdlem75  46624  fourierdlem79  46628  fourierdlem81  46630  fourierdlem82  46631  fourierdlem89  46638  fourierdlem90  46639  fourierdlem91  46640  fourierdlem93  46642  fourierdlem101  46650  fourierdlem111  46660  saldifcl  46762  unisalgen2  46797  hoidmv1lelem3  47036  smff  47175  sigardiv  47304  sigarcol  47307  sharhght  47308  sigaradd  47309  cevathlem1  47310  cevathlem2  47311  cevath  47312  proththd  48074  perfectALTVlem2  48195  gpgnbgrvtx0  48547  gpgnbgrvtx1  48548  imasubc2  49624  imaf1co  49627  idfullsubc  49633  fucofulem1  49782