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 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 206  df-an 397  df-3an 1089

This theorem is referenced by:  simp2bi  1146  f1dom3fv3dif  7220  f1dom3el3dif  7221  f1prex  7235  oeeui  8554  resixp  8878  domssex  9089  cantnflem1a  9630  cantnflem1d  9633  cantnflem3  9636  cantnflem4  9637  fpwwe2lem6  10581  canthnumlem  10593  canthp1lem2  10598  wun0  10663  lelttrdi  11326  supmullem2  12135  supmul  12136  ixxdisj  13289  ixxun  13290  ixxss1  13292  ixxss2  13293  ixxss12  13294  ixxub  13295  ixxlb  13296  ubioo  13306  elicore  13326  iccgelb  13330  iccss2  13345  icodisj  13403  xov1plusxeqvd  13425  fldiv  13775  immul  15033  sqrtge0  15154  sqrtrege0  15262  icco1  15434  ruclem2  16125  ruclem3  16126  ruclem8  16130  ruclem12  16134  gcddvds  16394  crth  16661  phimullem  16662  eulerthlem1  16664  eulerthlem2  16665  prmreclem3  16801  sectcan  17652  sectco  17653  sectmon  17679  monsect  17680  funcixp  17767  funcsect  17772  invfuc  17877  coapm  17971  catciso  18011  posasymb  18222  ipodrsima  18444  pstr2  18474  psdmrn  18476  psref  18477  mhmlin  18623  subm0cl  18636  eqger  18994  eqgcpbl  18998  gaorber  19102  orbstafun  19105  cayleyth  19211  pmtrrn2  19256  pmtrfinv  19257  dfod2  19360  sylow2blem1  19416  dprdf  19799  dprdff  19805  dprdfcl  19806  dprdsplit  19841  dpjcntz  19845  ablfac1a  19862  ablfac1b  19863  lmodvsdi  20402  lbssp  20597  2idlcpbl  20763  mpff  21551  mpfaddcl  21552  mpfmulcl  21553  mpfind  21554  pf1rcl  21752  mpfpf1  21754  mdetunilem2  21999  mdetunilem5  22002  mdetunilem6  22003  chfacfisfcpmat  22241  pnfnei  22608  cnptop2  22631  lmcl  22685  lmcnp  22692  flimfil  23357  tlmlmod  23577  ustbasel  23595  ustincl  23596  ustinvel  23598  ustfilxp  23601  tusunif  23658  imasdsf1olem  23763  xmeter  23823  tmsds  23877  metustexhalf  23949  nlmlmod  24079  qdensere  24170  blcvx  24198  tgqioo  24200  icccmplem2  24223  reconnlem1  24226  cnmpopc  24328  phtpcer  24395  phtpcco2  24399  pcohtpylem  24419  pcohtpy  24420  pcophtb  24429  om1addcl  24433  pi1blem  24439  pi1cpbl  24444  pi1grplem  24449  pi1inv  24452  pi1xfrf  24453  pi1xfr  24455  pi1xfrcnvlem  24456  pi1cof  24459  pi1coghm  24461  cphnlm  24573  cphsqrtcl2  24587  tcphcph  24638  lmcau  24714  bcthlem4  24728  minveclem4c  24826  minveclem2  24827  minveclem3b  24829  minveclem4  24833  minveclem6  24835  ivthicc  24859  ovolfsval  24871  ovollb2lem  24889  ovolshftlem1  24910  ovolscalem1  24914  ovolicc1  24917  ovolicc2lem2  24919  ovolicc2lem4  24921  ovolicc2lem5  24922  ovolicopnf  24925  ioombl1lem1  24959  ioombl1lem3  24961  ioombl1lem4  24962  uniioovol  24980  uniioombllem2a  24983  uniioombllem2  24984  uniioombllem3a  24985  uniioombllem3  24986  uniioombllem4  24987  uniioombllem6  24989  dyadmaxlem  24998  volivth  25008  vitalilem2  25010  vitalilem5  25013  i1frn  25078  itg2monolem1  25152  itgcnlem  25191  itgrevallem1  25196  itgreval  25198  itgle  25211  ibladd  25222  iblabslem  25229  itgspliticc  25238  itgsplitioo  25239  ditgcl  25259  ditgswap  25260  ditgsplitlem  25261  limcdif  25277  limcresi  25286  limccnp  25292  limccnp2  25293  limcco  25294  dvlip  25394  dvlip2  25396  dveq0  25401  dvgt0lem1  25403  dvivthlem1  25409  dvcnvrelem1  25418  dvcnvre  25420  dvfsumlem2  25428  ftc1lem1  25436  ftc1a  25438  ftc1lem4  25440  ftc2ditglem  25446  itgsubstlem  25449  ply1rem  25565  fta1glem1  25567  ig1pdvds  25578  plyrem  25702  facth  25703  fta1lem  25704  vieta1lem1  25707  vieta1lem2  25708  aaliou3lem3  25741  aaliou3lem4  25743  aaliou3lem7  25746  taylfvallem1  25753  tayl0  25758  taylply2  25764  radcnvle  25816  psercnlem2  25820  psercnlem1  25821  psercn  25822  pserdvlem1  25823  pserdvlem2  25824  abelth2  25838  coseq00topi  25896  coseq0negpitopi  25897  cosordlem  25923  tanord1  25930  efif1olem1  25935  loglesqrt  26148  logreclem  26149  relogbval  26159  nnlogbexp  26168  chordthmlem4  26222  quart1  26243  quartlem2  26245  quartlem3  26246  quartlem4  26247  quart  26248  acosbnd  26287  atancj  26297  atanlogsublem  26302  atantan  26310  atanbndlem  26312  dvatan  26322  atantayl  26324  rlimcnp2  26353  divsqrtsumlem  26366  ftalem5  26463  ftalem7  26465  basellem4  26470  basellem5  26471  perfectlem2  26615  dchrinv  26646  chpdifbndlem1  26938  pntibndlem2  26976  pntlemc  26980  pntlema  26981  pntlemb  26982  pntlemg  26983  pntlemh  26984  pntlemq  26986  pntlemr  26987  pntlemj  26988  pntlemi  26989  pntlemf  26990  pntlemk  26991  pntlemo  26992  pntleme  26993  pntlem3  26994  pntleml  26996  abvcxp  27000  scutun12  27192  slerec  27201  cofcut2  27284  cofcutr  27286  cofcutrtime  27289  addsproplem4  27327  addsproplem6  27329  addsunif  27353  addsasslem1  27354  addsasslem2  27355  negsproplem5  27373  negsproplem6  27374  negscut2  27381  negsunif  27393  axtgpasch  27472  cgr3simp2  27526  legso  27604  hlne2  27611  hlln  27612  mirhl  27684  inagswap  27846  inagne2  27848  dfcgrg2  27868  subumgredg2  28296  upgrres1  28324  nb3grprlem1  28391  wlkp  28627  wspthsswwlkn  28926  2wlkdlem6  28939  clwwisshclwwsn  29023  erclwwlkeqlen  29026  erclwwlksym  29028  erclwwlktr  29029  clwwlkn  29033  clwwlknwrd  29041  clwwlknonex2e  29117  grpoass  29508  vcsm  29567  nvf  29665  ssps  29735  minvecolem2  29880  minvecolem4c  29884  minvecolem4  29885  minvecolem5  29886  minvecolem6  29887  eigvec1  30967  eliccelico  31748  elicoelioo  31749  pmtrto1cl  32018  cyc3evpm  32069  slmdvsdi  32120  slmdvs1  32125  sdrgdvcl  32145  sdrginvcl  32146  fldgenssp  32156  imaslmod  32216  prmidlnr  32287  qsidomlem2  32302  mxidlnr  32309  0ringmon1p  32340  irngnzply1lem  32451  irngnzply1  32452  ply1annig1p  32460  ply1annprmidl  32462  cnre2csqlem  32580  lmxrge0  32622  sigaclci  32820  difelsiga  32821  insiga  32825  ldsysgenld  32848  sigapildsyslem  32849  sigapildsys  32850  ldgenpisyslem1  32851  measvnul  32894  sibfrn  33026  eulerpartlemt  33060  eulerpartlemmf  33064  tg5segofs  33375  lpadleft  33385  spthcycl  33810  subgrwlk  33813  acycgrcycl  33828  subfacp1lem2a  33861  subfacp1lem3  33863  subfacp1lem4  33864  subfacp1lem5  33865  sconnpht2  33919  sconnpi1  33920  resconn  33927  cvmsss  33948  cvmsn0  33949  cvmlift2lem3  33986  cvmlift2lem7  33990  cvmliftphtlem  33998  cvmliftpht  33999  cvmlift3lem5  34004  cvmlift3lem6  34005  msrf  34223  elmsta  34229  mclsax  34250  mthmpps  34263  mclspps  34265  ivthALT  34883  poimirlem17  36168  poimirlem20  36171  ibladdnc  36208  iblabsnclem  36214  ftc1cnnclem  36222  ftc1anc  36232  ftc2nc  36233  heiborlem3  36345  iccbnd  36372  rngohom1  36500  idl0cl  36550  maxidlnr  36574  lshpne  37517  opococ  37730  opexmid  37742  hlclat  37893  lclkrslem2  40074  fzne2d  40511  dvrelog2  40594  dvrelog3  40595  0nonelalab  40597  aks4d1p1p5  40605  metakunt8  40657  metakunt21  40670  metakunt22  40671  metakunt24  40673  metakunt25  40674  evlsval3  40802  flt4lem5f  41053  flt4lem7  41055  nna4b4nsq  41056  gneispacern2  42533  cvgdvgrat  42715  iccshift  43876  iccsuble  43877  icoiccdif  43882  mullimc  43977  limccog  43981  mullimcf  43984  lptioo2  43992  limcmptdm  43996  limcicciooub  43998  xlimmnfvlem1  44193  xlimpnfvlem1  44197  icccncfext  44248  cncfioobdlem  44257  ditgeqiooicc  44321  itgsubsticc  44337  iblcncfioo  44339  itgiccshift  44341  itgperiod  44342  itgsbtaddcnst  44343  stoweidlem31  44392  stoweidlem36  44397  stoweidlem38  44399  stoweidlem44  44405  stoweidlem62  44423  dirkercncflem1  44464  dirkercncflem4  44467  fourierdlem26  44494  fourierdlem32  44500  fourierdlem33  44501  fourierdlem37  44505  fourierdlem42  44510  fourierdlem54  44521  fourierdlem63  44530  fourierdlem64  44531  fourierdlem65  44532  fourierdlem69  44536  fourierdlem74  44541  fourierdlem75  44542  fourierdlem79  44546  fourierdlem81  44548  fourierdlem82  44549  fourierdlem89  44556  fourierdlem90  44557  fourierdlem91  44558  fourierdlem93  44560  fourierdlem101  44568  fourierdlem111  44578  saldifcl  44680  unisalgen2  44715  hoidmv1lelem3  44954  smff  45093  sigardiv  45222  sigarcol  45225  sharhght  45226  sigaradd  45227  cevathlem1  45228  cevathlem2  45229  cevath  45230  proththd  45926  perfectALTVlem2  46034