Theorem simp2d 1155

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

Syntax hints:   → wi 4   ∧ w3a 1097

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 209  df-an 400  df-3an 1099

This theorem is referenced by:  simp2bi  1158  f1dom3fv3dif  7246  f1dom3el3dif  7247  f1prex  7262  oeeui  8565  resixp  8909  domssex  9104  cantnflem1a  9635  cantnflem1d  9638  cantnflem3  9641  cantnflem4  9642  fpwwe2lem6  10589  canthnumlem  10601  canthp1lem2  10606  wun0  10671  lelttrdi  11340  supmullem2  12158  supmul  12159  ixxdisj  13359  ixxun  13360  ixxss1  13362  ixxss2  13363  ixxss12  13364  ixxub  13365  ixxlb  13366  ubioo  13376  elicore  13397  iccgelb  13401  iccss2  13416  icodisj  13475  xov1plusxeqvd  13497  fldiv  13865  immul  15144  sqrtge0  15265  sqrtrege0  15374  icco1  15548  ruclem2  16245  ruclem3  16246  ruclem8  16250  ruclem12  16254  gcddvds  16518  crth  16794  phimullem  16795  eulerthlem1  16797  eulerthlem2  16798  prmreclem3  16935  sectcan  17769  sectco  17770  sectmon  17796  monsect  17797  funcixp  17881  funcsect  17886  invfuc  17991  coapm  18085  catciso  18125  posasymb  18332  ipodrsima  18554  pstr2  18584  psdmrn  18586  psref  18587  mhmlin  18808  subm0cl  18826  eqger  19200  eqgcpbl  19204  gaorber  19329  orbstafun  19332  cayleyth  19436  pmtrrn2  19481  pmtrfinv  19482  dfod2  19585  sylow2blem1  19641  dprdf  20029  dprdff  20035  dprdfcl  20036  dprdsplit  20071  dpjcntz  20075  ablfac1a  20092  ablfac1b  20093  lmodvsdi  20930  lbssp  21124  2idlcpblrng  21319  evlsval3  22120  mpff  22143  mpfaddcl  22144  mpfmulcl  22145  mpfind  22146  pf1rcl  22390  mpfpf1  22392  mdetunilem2  22651  mdetunilem5  22654  mdetunilem6  22655  chfacfisfcpmat  22893  pnfnei  23258  cnptop2  23281  lmcl  23335  lmcnp  23342  flimfil  24007  tlmlmod  24227  ustbasel  24245  ustincl  24246  ustinvel  24248  ustfilxp  24251  tusunif  24306  imasdsf1olem  24411  xmeter  24471  tmsds  24522  metustexhalf  24594  nlmlmod  24716  qdensere  24807  blcvx  24836  tgqioo  24838  icccmplem2  24862  reconnlem1  24865  cnmpopc  24968  phtpcer  25035  phtpcco2  25039  pcohtpylem  25059  pcohtpy  25060  pcophtb  25069  om1addcl  25073  pi1blem  25079  pi1cpbl  25084  pi1grplem  25089  pi1inv  25092  pi1xfrf  25093  pi1xfr  25095  pi1xfrcnvlem  25096  pi1cof  25099  pi1coghm  25101  cphnlm  25212  cphsqrtcl2  25226  tcphcph  25277  lmcau  25353  bcthlem4  25367  minveclem4c  25465  minveclem2  25466  minveclem3b  25468  minveclem4  25472  minveclem6  25474  ivthicc  25498  ovolfsval  25510  ovollb2lem  25528  ovolshftlem1  25549  ovolscalem1  25553  ovolicc1  25556  ovolicc2lem2  25558  ovolicc2lem4  25560  ovolicc2lem5  25561  ovolicopnf  25564  ioombl1lem1  25598  ioombl1lem3  25600  ioombl1lem4  25601  uniioovol  25619  uniioombllem2a  25622  uniioombllem2  25623  uniioombllem3a  25624  uniioombllem3  25625  uniioombllem4  25626  uniioombllem6  25628  dyadmaxlem  25637  volivth  25647  vitalilem2  25649  vitalilem5  25652  i1frn  25717  itg2monolem1  25790  itgcnlem  25830  itgrevallem1  25835  itgreval  25837  itgle  25850  ibladd  25861  iblabslem  25868  itgspliticc  25877  itgsplitioo  25878  ditgcl  25898  ditgswap  25899  ditgsplitlem  25900  limcdif  25916  limcresi  25925  limccnp  25931  limccnp2  25932  limcco  25933  dvlip  26033  dvlip2  26035  dveq0  26040  dvgt0lem1  26042  dvivthlem1  26048  dvcnvrelem1  26057  dvcnvre  26059  dvfsumlem2  26067  ftc1lem1  26075  ftc1a  26077  ftc1lem4  26079  ftc2ditglem  26085  itgsubstlem  26088  ply1rem  26204  fta1glem1  26206  ig1pdvds  26218  plyrem  26344  facth  26345  fta1lem  26346  vieta1lem1  26349  vieta1lem2  26350  aaliou3lem3  26383  aaliou3lem4  26385  aaliou3lem7  26388  taylfvallem1  26395  tayl0  26400  taylply2  26406  radcnvle  26458  psercnlem2  26462  psercnlem1  26463  psercn  26464  pserdvlem1  26465  pserdvlem2  26466  abelth2  26480  coseq00topi  26542  coseq0negpitopi  26543  cosordlem  26570  tanord1  26577  efif1olem1  26582  loglesqrt  26801  logreclem  26802  relogbval  26812  nnlogbexp  26821  chordthmlem4  26875  quart1  26896  quartlem2  26898  quartlem3  26899  quartlem4  26900  quart  26901  acosbnd  26940  atancj  26950  atanlogsublem  26955  atantan  26963  atanbndlem  26965  dvatan  26975  atantayl  26977  rlimcnp2  27006  divsqrtsumlem  27019  ftalem5  27116  ftalem7  27118  basellem4  27123  basellem5  27124  perfectlem2  27269  dchrinv  27300  chpdifbndlem1  27592  pntibndlem2  27630  pntlemc  27634  pntlema  27635  pntlemb  27636  pntlemg  27637  pntlemh  27638  pntlemq  27640  pntlemr  27641  pntlemj  27642  pntlemi  27643  pntlemf  27644  pntlemk  27645  pntlemo  27646  pntleme  27647  pntlem3  27648  pntleml  27650  abvcxp  27654  cutsun12  27858  lesrec  27867  eqcuts3  27872  cofcut2  27990  cofcutr  27992  cofcutrtime  27995  cutmax  28002  cutmin  28003  addsproplem4  28040  addsproplem6  28042  addsuniflem  28069  addsasslem1  28071  addsasslem2  28072  negsproplem5  28100  negsproplem6  28101  negcut2  28108  negsunif  28123  mulsproplem12  28195  sltmuls1  28215  sltmuls2  28216  mulsuniflem  28217  precsexlem11  28285  twocut  28491  pw2cut2  28530  axtgpasch  28611  cgr3simp2  28665  legso  28743  hlne2  28750  hlln  28751  mirhl  28823  inagswap  28985  inagne2  28987  dfcgrg2  29007  subumgredg2  29430  upgrres1  29458  nb3grprlem1  29525  wlkp  29761  wspthsswwlkn  30062  2wlkdlem6  30075  clwwisshclwwsn  30162  erclwwlkeqlen  30165  erclwwlksym  30167  erclwwlktr  30168  clwwlkn  30172  clwwlknwrd  30180  clwwlknonex2e  30256  grpoass  30650  vcsm  30709  nvf  30807  ssps  30877  minvecolem2  31022  minvecolem4c  31026  minvecolem4  31027  minvecolem5  31028  minvecolem6  31029  eigvec1  32109  eliccelico  32927  elicoelioo  32928  pmtrto1cl  33238  cyc3evpm  33289  slmdvsdi  33354  slmdvs1  33359  sdrgdvcl  33445  sdrginvcl  33446  fldgenssp  33464  imaslmod  33498  prmidlnr  33584  qsidomlem2  33599  mxidlnr  33611  0ringmon1p  33712  irngnzply1lem  33946  irngnzply1  33947  ply1annig1p  33960  minplycl  33962  ply1annprmidl  33963  minplym1p  33969  minplynzm1p  33970  algextdeglem1  33973  algextdeglem2  33974  algextdeglem3  33975  algextdeglem4  33976  algextdeglem5  33977  constrsqrtcl  34035  cnre2csqlem  34166  lmxrge0  34208  sigaclci  34388  difelsiga  34389  insiga  34393  ldsysgenld  34416  sigapildsyslem  34417  sigapildsys  34418  ldgenpisyslem1  34419  measvnul  34462  sibfrn  34593  eulerpartlemt  34627  eulerpartlemmf  34631  tg5segofs  34932  lpadleft  34942  spthcycl  35432  subgrwlk  35435  acycgrcycl  35450  subfacp1lem2a  35483  subfacp1lem3  35485  subfacp1lem4  35486  subfacp1lem5  35487  sconnpht2  35541  sconnpi1  35542  resconn  35549  cvmsss  35570  cvmsn0  35571  cvmlift2lem3  35608  cvmlift2lem7  35612  cvmliftphtlem  35620  cvmliftpht  35621  cvmlift3lem5  35626  cvmlift3lem6  35627  msrf  35845  elmsta  35851  mclsax  35872  mthmpps  35885  mclspps  35887  ivthALT  36648  weiunpo  36778  weiunso  36779  weiunfr  36780  weiunse  36781  poimirlem17  38089  poimirlem20  38092  ibladdnc  38129  iblabsnclem  38135  ftc1cnnclem  38143  ftc1anc  38153  ftc2nc  38154  heiborlem3  38265  iccbnd  38292  rngohom1  38420  idl0cl  38470  maxidlnr  38494  lshpne  39559  opococ  39772  opexmid  39784  hlclat  39935  lclkrslem2  42115  fzne2d  42550  dvrelog2  42634  dvrelog3  42635  0nonelalab  42637  aks4d1p1p5  42645  primrootsunit1  42667  primrootscoprmpow  42669  primrootscoprbij  42672  primrootspoweq0  42676  aks6d1c2lem3  42696  aks6d1c2  42700  aks6d1c6lem5  42747  aks5lem1  42756  aks5lem2  42757  aks5lem3a  42759  aks5lem5a  42761  unitscyglem1  42765  flt4lem5f  43192  flt4lem7  43194  nna4b4nsq  43195  gneispacern2  44668  cvgdvgrat  44842  iccshift  46047  iccsuble  46048  icoiccdif  46053  mullimc  46145  limccog  46149  mullimcf  46152  lptioo2  46160  limcmptdm  46162  limcicciooub  46164  xlimmnfvlem1  46359  xlimpnfvlem1  46363  icccncfext  46414  cncfioobdlem  46423  ditgeqiooicc  46487  itgsubsticc  46503  iblcncfioo  46505  itgiccshift  46507  itgperiod  46508  itgsbtaddcnst  46509  stoweidlem31  46558  stoweidlem36  46563  stoweidlem38  46565  stoweidlem44  46571  stoweidlem62  46589  dirkercncflem1  46630  dirkercncflem4  46633  fourierdlem26  46660  fourierdlem32  46666  fourierdlem33  46667  fourierdlem37  46671  fourierdlem42  46676  fourierdlem54  46687  fourierdlem63  46696  fourierdlem64  46697  fourierdlem65  46698  fourierdlem69  46702  fourierdlem74  46707  fourierdlem75  46708  fourierdlem79  46712  fourierdlem81  46714  fourierdlem82  46715  fourierdlem89  46722  fourierdlem90  46723  fourierdlem91  46724  fourierdlem93  46726  fourierdlem101  46734  fourierdlem111  46744  saldifcl  46846  unisalgen2  46881  hoidmv1lelem3  47120  smff  47259  sigardiv  47388  sigarcol  47391  sharhght  47392  sigaradd  47393  cevathlem1  47394  cevathlem2  47395  cevath  47396  proththd  48176  perfectALTVlem2  48297  gpgnbgrvtx0  48649  gpgnbgrvtx1  48650  imasubc2  49726  imaf1co  49729  idfullsubc  49735  fucofulem1  49884