Theorem simp2d 1179

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

Syntax hints:   → wi 4   ∧ w3a 1113

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 199  df-an 387  df-3an 1115

This theorem is referenced by:  simp2bi  1182  f1dom3fv3dif  6780  f1dom3el3dif  6781  f1prex  6794  oeeui  7949  resixp  8210  domssex  8390  cantnflem1a  8859  cantnflem1d  8862  cantnflem3  8865  cantnflem4  8866  fpwwe2lem7  9773  canthnumlem  9785  canthp1lem2  9790  wun0  9855  lelttrdi  10518  supmullem2  11324  supmul  11325  ixxdisj  12478  ixxun  12479  ixxss1  12481  ixxss2  12482  ixxss12  12483  ixxub  12484  ixxlb  12485  ubioo  12495  elicore  12514  iccgelb  12518  iccss2  12532  icodisj  12588  xov1plusxeqvd  12611  fldiv  12954  immul  14253  sqrtge0  14375  sqrtrege0  14482  icco1  14648  ruclem2  15335  ruclem3  15336  ruclem8  15340  ruclem12  15344  gcddvds  15598  crth  15854  phimullem  15855  eulerthlem1  15857  eulerthlem2  15858  prmreclem3  15993  sectcan  16767  sectco  16768  sectmon  16794  monsect  16795  funcixp  16879  funcsect  16884  invfuc  16986  coapm  17073  catciso  17109  posasymb  17305  ipodrsima  17518  pstr2  17558  psdmrn  17560  psref  17561  mhmlin  17695  subm0cl  17705  eqger  17995  eqgcpbl  17999  gaorber  18091  orbstafun  18094  cayleyth  18185  pmtrrn2  18230  pmtrfinv  18231  dfod2  18332  sylow2blem1  18386  dprdf  18759  dprdff  18765  dprdfcl  18766  dprdsplit  18801  dpjcntz  18805  ablfac1a  18822  ablfac1b  18823  lmodvsdi  19242  lbssp  19438  2idlcpbl  19595  assaring  19681  mpff  19893  mpfaddcl  19894  mpfmulcl  19895  mpfind  19896  pf1rcl  20073  mpfpf1  20075  mdetunilem2  20787  mdetunilem5  20790  mdetunilem6  20791  chfacfisfcpmat  21030  pnfnei  21395  cnptop2  21418  lmcl  21472  lmcnp  21479  flimfil  22143  tlmlmod  22362  ustbasel  22380  ustincl  22381  ustinvel  22383  ustfilxp  22386  tusunif  22443  imasdsf1olem  22548  xmeter  22608  tmsds  22659  metustexhalf  22731  nlmlmod  22852  qdensere  22943  blcvx  22971  tgqioo  22973  icccmplem2  22996  reconnlem1  22999  cnmpt2pc  23097  phtpcer  23164  phtpcco2  23168  pcohtpylem  23188  pcohtpy  23189  pcophtb  23198  om1addcl  23202  pi1blem  23208  pi1cpbl  23213  pi1grplem  23218  pi1inv  23221  pi1xfrf  23222  pi1xfr  23224  pi1xfrcnvlem  23225  pi1cof  23228  pi1coghm  23230  cphnlm  23341  cphsqrtcl2  23355  tcphcph  23405  lmcau  23481  bcthlem4  23495  minveclem4c  23593  minveclem2  23594  minveclem3b  23596  minveclem4  23600  minveclem6  23602  ivthicc  23624  ovolfsval  23636  ovollb2lem  23654  ovolshftlem1  23675  ovolscalem1  23679  ovolicc1  23682  ovolicc2lem2  23684  ovolicc2lem4  23686  ovolicc2lem5  23687  ovolicopnf  23690  ioombl1lem1  23724  ioombl1lem3  23726  ioombl1lem4  23727  uniioovol  23745  uniioombllem2a  23748  uniioombllem2  23749  uniioombllem3a  23750  uniioombllem3  23751  uniioombllem4  23752  uniioombllem6  23754  dyadmaxlem  23763  volivth  23773  vitalilem2  23775  vitalilem5  23778  i1frn  23843  itg2monolem1  23916  itgcnlem  23955  itgrevallem1  23960  itgreval  23962  itgle  23975  ibladd  23986  iblabslem  23993  itgspliticc  24002  itgsplitioo  24003  ditgcl  24021  ditgswap  24022  ditgsplitlem  24023  limcdif  24039  limcresi  24048  limccnp  24054  limccnp2  24055  limcco  24056  dvlip  24155  dvlip2  24157  dveq0  24162  dvgt0lem1  24164  dvivthlem1  24170  dvcnvrelem1  24179  dvcnvre  24181  dvfsumlem2  24189  ftc1lem1  24197  ftc1a  24199  ftc1lem4  24201  ftc2ditglem  24207  itgsubstlem  24210  ply1rem  24322  fta1glem1  24324  ig1pdvds  24335  plyrem  24459  facth  24460  fta1lem  24461  vieta1lem1  24464  vieta1lem2  24465  aaliou3lem3  24498  aaliou3lem4  24500  aaliou3lem7  24503  taylfvallem1  24510  tayl0  24515  taylply2  24521  radcnvle  24573  psercnlem2  24577  psercnlem1  24578  psercn  24579  pserdvlem1  24580  pserdvlem2  24581  abelth2  24595  coseq00topi  24654  coseq0negpitopi  24655  cosordlem  24677  tanord1  24683  efif1olem1  24688  loglesqrt  24901  logreclem  24902  relogbval  24912  nnlogbexp  24921  chordthmlem4  24975  quart1  24996  quartlem2  24998  quartlem3  24999  quartlem4  25000  quart  25001  acosbnd  25040  atancj  25050  atanlogsublem  25055  atantan  25063  atanbndlem  25065  dvatan  25075  atantayl  25077  rlimcnp2  25106  divsqrtsumlem  25119  ftalem5  25216  ftalem7  25218  basellem4  25223  basellem5  25224  perfectlem2  25368  dchrinv  25399  chpdifbndlem1  25655  pntibndlem2  25693  pntlemc  25697  pntlema  25698  pntlemb  25699  pntlemg  25700  pntlemh  25701  pntlemq  25703  pntlemr  25704  pntlemj  25705  pntlemi  25706  pntlemf  25707  pntlemk  25708  pntlemo  25709  pntleme  25710  pntlem3  25711  pntleml  25713  abvcxp  25717  axtgpasch  25779  cgr3simp2  25833  legso  25911  hlne2  25918  hlln  25919  mirhl  25991  hlperpnel  26034  opphllem4  26059  inagswap  26148  dfcgrg2  26162  subumgredg2  26582  upgrres1  26610  nb3grprlem1  26678  wlkp  26914  wspthsswwlkn  27247  2wlkdlem6  27260  clwwisshclwwsn  27354  erclwwlkeqlen  27357  erclwwlksym  27359  erclwwlktr  27360  clwwlkn  27366  clwwlknwrd  27377  clwwlknonex2e  27485  grpoass  27913  vcsm  27972  nvf  28070  ssps  28140  minvecolem2  28286  minvecolem4c  28290  minvecolem4  28291  minvecolem5  28292  minvecolem6  28293  eigvec1  29376  eliccelico  30086  elicoelioo  30087  slmdvsdi  30313  slmdvs1  30318  pmtrto1cl  30394  cnre2csqlem  30501  lmxrge0  30543  sigaclci  30740  difelsiga  30741  insiga  30745  ldsysgenld  30768  sigapildsyslem  30769  sigapildsys  30770  ldgenpisyslem1  30771  measvnul  30814  sibfrn  30944  eulerpartlemt  30978  eulerpartlemmf  30982  tg5segofs  31300  subfacp1lem2a  31708  subfacp1lem3  31710  subfacp1lem4  31711  subfacp1lem5  31712  sconnpht2  31766  sconnpi1  31767  resconn  31774  cvmsss  31795  cvmsn0  31796  cvmlift2lem3  31833  cvmlift2lem7  31837  cvmliftphtlem  31845  cvmliftpht  31846  cvmlift3lem5  31851  cvmlift3lem6  31852  msrf  31985  elmsta  31991  mclsax  32012  mthmpps  32025  mclspps  32027  scutun12  32456  slerec  32462  ivthALT  32868  poimirlem17  33970  poimirlem20  33973  ibladdnc  34010  iblabsnclem  34016  ftc1cnnclem  34026  ftc1anc  34036  ftc2nc  34037  heiborlem3  34154  iccbnd  34181  rngohom1  34309  idl0cl  34359  maxidlnr  34383  lshpne  35057  opococ  35270  opexmid  35282  hlclat  35433  lclkrslem2  37613  gneispacern2  39277  cvgdvgrat  39352  iccshift  40540  iccsuble  40541  icoiccdif  40546  mullimc  40643  limccog  40647  mullimcf  40650  lptioo2  40658  limcmptdm  40662  limcicciooub  40664  xlimmnfvlem1  40853  xlimpnfvlem1  40857  icccncfext  40895  cncfioobdlem  40904  ditgeqiooicc  40970  itgsubsticc  40986  iblcncfioo  40988  itgiccshift  40990  itgperiod  40991  itgsbtaddcnst  40992  stoweidlem11  41022  stoweidlem31  41042  stoweidlem36  41047  stoweidlem38  41049  stoweidlem44  41055  stoweidlem62  41073  dirkercncflem1  41114  dirkercncflem4  41117  fourierdlem26  41144  fourierdlem32  41150  fourierdlem33  41151  fourierdlem37  41155  fourierdlem42  41160  fourierdlem54  41171  fourierdlem63  41180  fourierdlem64  41181  fourierdlem65  41182  fourierdlem69  41186  fourierdlem74  41191  fourierdlem75  41192  fourierdlem79  41196  fourierdlem81  41198  fourierdlem82  41199  fourierdlem89  41206  fourierdlem90  41207  fourierdlem91  41208  fourierdlem93  41210  fourierdlem101  41218  fourierdlem111  41228  saldifcl  41330  unisalgen2  41363  hoidmv1lelem3  41601  smff  41735  smfpimltxr  41750  sigardiv  41844  sigarcol  41847  sharhght  41848  sigaradd  41849  cevathlem1  41850  cevathlem2  41851  cevath  41852  proththd  42361  perfectALTVlem2  42461