Theorem simp2d 1159

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

Syntax hints:   → wi 4   ∧ w3a 1101

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 210  df-an 401  df-3an 1103

This theorem is referenced by:  simp2bi  1162  f1dom3fv3dif  7256  f1dom3el3dif  7257  f1prex  7272  oeeui  8576  resixp  8919  domssex  9114  cantnflem1a  9642  cantnflem1d  9645  cantnflem3  9648  cantnflem4  9649  fpwwe2lem6  10609  canthnumlem  10621  canthp1lem2  10626  wun0  10691  lelttrdi  11360  supmullem2  12177  supmul  12178  ixxdisj  13378  ixxun  13379  ixxss1  13381  ixxss2  13382  ixxss12  13383  ixxub  13384  ixxlb  13385  ubioo  13395  elicore  13416  iccgelb  13420  iccss2  13435  icodisj  13494  xov1plusxeqvd  13516  fldiv  13884  immul  15177  sqrtge0  15298  sqrtrege0  15407  icco1  15581  ruclem2  16278  ruclem3  16279  ruclem8  16283  ruclem12  16287  gcddvds  16551  crth  16827  phimullem  16828  eulerthlem1  16830  eulerthlem2  16831  prmreclem3  16968  sectcan  17802  sectco  17803  sectmon  17829  monsect  17830  funcixp  17914  funcsect  17919  invfuc  18024  coapm  18118  catciso  18158  posasymb  18365  ipodrsima  18587  pstr2  18617  psdmrn  18619  psref  18620  mhmlin  18841  subm0cl  18859  eqger  19237  eqgcpbl  19241  gaorber  19369  orbstafun  19372  cayleyth  19476  pmtrrn2  19521  pmtrfinv  19522  dfod2  19625  sylow2blem1  19681  dprdf  20069  dprdff  20075  dprdfcl  20076  dprdsplit  20111  dpjcntz  20115  ablfac1a  20132  ablfac1b  20133  lmodvsdi  20975  lbssp  21169  2idlcpblrng  21372  prmidlnr  21426  qsidomlem2  21441  evlsval3  22200  mpff  22223  mpfaddcl  22224  mpfmulcl  22225  mpfind  22226  pf1rcl  22470  mpfpf1  22472  mdetunilem2  22731  mdetunilem5  22734  mdetunilem6  22735  chfacfisfcpmat  22973  pnfnei  23338  cnptop2  23361  lmcl  23415  lmcnp  23422  flimfil  24087  tlmlmod  24307  ustbasel  24325  ustincl  24326  ustinvel  24328  ustfilxp  24331  tusunif  24386  imasdsf1olem  24491  xmeter  24551  tmsds  24602  metustexhalf  24674  nlmlmod  24796  qdensere  24887  blcvx  24916  tgqioo  24918  icccmplem2  24942  reconnlem1  24945  cnmpopc  25048  phtpcer  25115  phtpcco2  25119  pcohtpylem  25139  pcohtpy  25140  pcophtb  25149  om1addcl  25153  pi1blem  25159  pi1cpbl  25164  pi1grplem  25169  pi1inv  25172  pi1xfrf  25173  pi1xfr  25175  pi1xfrcnvlem  25176  pi1cof  25179  pi1coghm  25181  cphnlm  25292  cphsqrtcl2  25306  tcphcph  25357  lmcau  25433  bcthlem4  25447  minveclem4c  25545  minveclem2  25546  minveclem3b  25548  minveclem4  25552  minveclem6  25554  ivthicc  25578  ovolfsval  25590  ovollb2lem  25608  ovolshftlem1  25629  ovolscalem1  25633  ovolicc1  25636  ovolicc2lem2  25638  ovolicc2lem4  25640  ovolicc2lem5  25641  ovolicopnf  25644  ioombl1lem1  25678  ioombl1lem3  25680  ioombl1lem4  25681  uniioovol  25699  uniioombllem2a  25702  uniioombllem2  25703  uniioombllem3a  25704  uniioombllem3  25705  uniioombllem4  25706  uniioombllem6  25708  dyadmaxlem  25717  volivth  25727  vitalilem2  25729  vitalilem5  25732  i1frn  25797  itg2monolem1  25870  itgcnlem  25910  itgrevallem1  25915  itgreval  25917  itgle  25930  ibladd  25941  iblabslem  25948  itgspliticc  25957  itgsplitioo  25958  ditgcl  25978  ditgswap  25979  ditgsplitlem  25980  limcdif  25996  limcresi  26005  limccnp  26011  limccnp2  26012  limcco  26013  dvlip  26113  dvlip2  26115  dveq0  26120  dvgt0lem1  26122  dvivthlem1  26128  dvcnvrelem1  26137  dvcnvre  26139  dvfsumlem2  26147  ftc1lem1  26155  ftc1a  26157  ftc1lem4  26159  ftc2ditglem  26165  itgsubstlem  26168  ply1rem  26284  fta1glem1  26286  ig1pdvds  26298  plyrem  26427  facth  26428  fta1lem  26429  vieta1lem1  26432  vieta1lem2  26433  aaliou3lem3  26466  aaliou3lem4  26468  aaliou3lem7  26471  taylfvallem1  26478  tayl0  26483  taylply2  26489  radcnvle  26541  psercnlem2  26545  psercnlem1  26546  psercn  26547  pserdvlem1  26548  pserdvlem2  26549  abelth2  26563  coseq00topi  26625  coseq0negpitopi  26626  cosordlem  26653  tanord1  26660  efif1olem1  26665  loglesqrt  26884  logreclem  26885  relogbval  26895  nnlogbexp  26904  chordthmlem4  26958  quart1  26979  quartlem2  26981  quartlem3  26982  quartlem4  26983  quart  26984  acosbnd  27023  atancj  27033  atanlogsublem  27038  atantan  27046  atanbndlem  27048  dvatan  27058  atantayl  27060  rlimcnp2  27089  divsqrtsumlem  27102  ftalem5  27199  ftalem7  27201  basellem4  27206  basellem5  27207  perfectlem2  27352  dchrinv  27383  chpdifbndlem1  27675  pntibndlem2  27713  pntlemc  27717  pntlema  27718  pntlemb  27719  pntlemg  27720  pntlemh  27721  pntlemq  27723  pntlemr  27724  pntlemj  27725  pntlemi  27726  pntlemf  27727  pntlemk  27728  pntlemo  27729  pntleme  27730  pntlem3  27731  pntleml  27733  abvcxp  27737  cutsun12  27941  lesrec  27950  eqcuts3  27955  cofcut2  28073  cofcutr  28075  cofcutrtime  28078  cutmax  28085  cutmin  28086  addsproplem4  28123  addsproplem6  28125  addsuniflem  28152  addsasslem1  28154  addsasslem2  28155  negsproplem5  28183  negsproplem6  28184  negcut2  28191  negsunif  28206  mulsproplem12  28278  sltmuls1  28298  sltmuls2  28299  mulsuniflem  28300  precsexlem11  28368  twocut  28574  pw2cut2  28613  axtgpasch  28694  cgr3simp2  28748  legso  28826  hlne2  28833  hlln  28834  mirhl  28910  inagswap  29093  inagne2  29095  dfcgrg2  29115  subumgredg2  29544  upgrres1  29572  nb3grprlem1  29639  wlkp  29875  wspthsswwlkn  30176  2wlkdlem6  30189  clwwisshclwwsn  30276  erclwwlkeqlen  30279  erclwwlksym  30281  erclwwlktr  30282  clwwlkn  30286  clwwlknwrd  30294  clwwlknonex2e  30370  grpoass  30764  vcsm  30823  nvf  30921  ssps  30991  minvecolem2  31136  minvecolem4c  31140  minvecolem4  31141  minvecolem5  31142  minvecolem6  31143  eigvec1  32223  eliccelico  33034  elicoelioo  33035  pmtrto1cl  33332  cyc3evpm  33383  slmdvsdi  33448  slmdvs1  33453  sdrgdvcl  33535  sdrginvcl  33536  fldgenssp  33554  imaslmod  33588  mxidlnr  33664  0ringmon1p  33764  irngnzply1lem  33997  irngnzply1  33998  ply1annig1p  34011  minplycl  34013  ply1annprmidl  34014  minplym1p  34020  minplynzm1p  34021  algextdeglem1  34024  algextdeglem2  34025  algextdeglem3  34026  algextdeglem4  34027  algextdeglem5  34028  constrsqrtcl  34086  cnre2csqlem  34217  lmxrge0  34259  sigaclci  34439  difelsiga  34440  insiga  34444  ldsysgenld  34467  sigapildsyslem  34468  sigapildsys  34469  ldgenpisyslem1  34470  measvnul  34513  sibfrn  34644  eulerpartlemt  34678  eulerpartlemmf  34682  tg5segofs  34980  lpadleft  34990  spthcycl  35492  subgrwlk  35495  acycgrcycl  35510  subfacp1lem2a  35543  subfacp1lem3  35545  subfacp1lem4  35546  subfacp1lem5  35547  sconnpht2  35601  sconnpi1  35602  resconn  35609  cvmsss  35630  cvmsn0  35631  cvmlift2lem3  35668  cvmlift2lem7  35672  cvmliftphtlem  35680  cvmliftpht  35681  cvmlift3lem5  35686  cvmlift3lem6  35687  msrf  35905  elmsta  35911  mclsax  35932  mthmpps  35945  mclspps  35947  ivthALT  36708  weiunpo  36838  weiunso  36839  weiunfr  36840  weiunse  36841  poimirlem17  38148  poimirlem20  38151  ibladdnc  38188  iblabsnclem  38194  ftc1cnnclem  38202  ftc1anc  38212  ftc2nc  38213  heiborlem3  38324  iccbnd  38351  rngohom1  38479  idl0cl  38529  maxidlnr  38553  lshpne  39618  opococ  39831  opexmid  39843  hlclat  39994  lclkrslem2  42174  fzne2d  42609  dvrelog2  42693  dvrelog3  42694  0nonelalab  42696  aks4d1p1p5  42704  primrootsunit1  42726  primrootscoprmpow  42728  primrootscoprbij  42731  primrootspoweq0  42735  aks6d1c2lem3  42755  aks6d1c2  42759  aks6d1c6lem5  42806  aks5lem1  42815  aks5lem2  42816  aks5lem3a  42818  aks5lem5a  42820  unitscyglem1  42824  flt4lem5f  43251  flt4lem7  43253  nna4b4nsq  43254  gneispacern2  44727  cvgdvgrat  44887  iccshift  46092  iccsuble  46093  icoiccdif  46098  mullimc  46190  limccog  46194  mullimcf  46197  lptioo2  46205  limcmptdm  46207  limcicciooub  46209  xlimmnfvlem1  46404  xlimpnfvlem1  46408  icccncfext  46459  cncfioobdlem  46468  ditgeqiooicc  46532  itgsubsticc  46548  iblcncfioo  46550  itgiccshift  46552  itgperiod  46553  itgsbtaddcnst  46554  stoweidlem31  46603  stoweidlem36  46608  stoweidlem38  46610  stoweidlem44  46616  stoweidlem62  46634  dirkercncflem1  46675  dirkercncflem4  46678  fourierdlem26  46705  fourierdlem32  46711  fourierdlem33  46712  fourierdlem37  46716  fourierdlem42  46721  fourierdlem54  46732  fourierdlem63  46741  fourierdlem64  46742  fourierdlem65  46743  fourierdlem69  46747  fourierdlem74  46752  fourierdlem75  46753  fourierdlem79  46757  fourierdlem81  46759  fourierdlem82  46760  fourierdlem89  46767  fourierdlem90  46768  fourierdlem91  46769  fourierdlem93  46771  fourierdlem101  46779  fourierdlem111  46789  saldifcl  46891  unisalgen2  46926  hoidmv1lelem3  47165  smff  47304  sigardiv  47433  sigarcol  47436  sharhght  47437  sigaradd  47438  cevathlem1  47439  cevathlem2  47440  cevath  47441  proththd  48221  perfectALTVlem2  48342  gpgnbgrvtx0  48694  gpgnbgrvtx1  48695  imasubc2  49781  imaf1co  49784  idfullsubc  49790  fucofulem1  49939