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 1086

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 1088

This theorem is referenced by:  simp2bi  1146  f1dom3fv3dif  7260  f1dom3el3dif  7261  f1prex  7276  oeeui  8612  resixp  8945  domssex  9150  cantnflem1a  9697  cantnflem1d  9700  cantnflem3  9703  cantnflem4  9704  fpwwe2lem6  10648  canthnumlem  10660  canthp1lem2  10665  wun0  10730  lelttrdi  11395  supmullem2  12211  supmul  12212  ixxdisj  13375  ixxun  13376  ixxss1  13378  ixxss2  13379  ixxss12  13380  ixxub  13381  ixxlb  13382  ubioo  13392  elicore  13413  iccgelb  13417  iccss2  13432  icodisj  13491  xov1plusxeqvd  13513  fldiv  13875  immul  15153  sqrtge0  15274  sqrtrege0  15382  icco1  15554  ruclem2  16248  ruclem3  16249  ruclem8  16253  ruclem12  16257  gcddvds  16520  crth  16795  phimullem  16796  eulerthlem1  16798  eulerthlem2  16799  prmreclem3  16936  sectcan  17766  sectco  17767  sectmon  17793  monsect  17794  funcixp  17878  funcsect  17883  invfuc  17988  coapm  18082  catciso  18122  posasymb  18329  ipodrsima  18549  pstr2  18579  psdmrn  18581  psref  18582  mhmlin  18769  subm0cl  18787  eqger  19159  eqgcpbl  19163  gaorber  19289  orbstafun  19292  cayleyth  19394  pmtrrn2  19439  pmtrfinv  19440  dfod2  19543  sylow2blem1  19599  dprdf  19987  dprdff  19993  dprdfcl  19994  dprdsplit  20029  dpjcntz  20033  ablfac1a  20050  ablfac1b  20051  lmodvsdi  20840  lbssp  21035  2idlcpblrng  21230  mpff  22060  mpfaddcl  22061  mpfmulcl  22062  mpfind  22063  pf1rcl  22285  mpfpf1  22287  mdetunilem2  22549  mdetunilem5  22552  mdetunilem6  22553  chfacfisfcpmat  22791  pnfnei  23156  cnptop2  23179  lmcl  23233  lmcnp  23240  flimfil  23905  tlmlmod  24125  ustbasel  24143  ustincl  24144  ustinvel  24146  ustfilxp  24149  tusunif  24205  imasdsf1olem  24310  xmeter  24370  tmsds  24421  metustexhalf  24493  nlmlmod  24615  qdensere  24706  blcvx  24735  tgqioo  24737  icccmplem2  24761  reconnlem1  24764  cnmpopc  24871  phtpcer  24943  phtpcco2  24948  pcohtpylem  24968  pcohtpy  24969  pcophtb  24978  om1addcl  24982  pi1blem  24988  pi1cpbl  24993  pi1grplem  24998  pi1inv  25001  pi1xfrf  25002  pi1xfr  25004  pi1xfrcnvlem  25005  pi1cof  25008  pi1coghm  25010  cphnlm  25122  cphsqrtcl2  25136  tcphcph  25187  lmcau  25263  bcthlem4  25277  minveclem4c  25375  minveclem2  25376  minveclem3b  25378  minveclem4  25382  minveclem6  25384  ivthicc  25409  ovolfsval  25421  ovollb2lem  25439  ovolshftlem1  25460  ovolscalem1  25464  ovolicc1  25467  ovolicc2lem2  25469  ovolicc2lem4  25471  ovolicc2lem5  25472  ovolicopnf  25475  ioombl1lem1  25509  ioombl1lem3  25511  ioombl1lem4  25512  uniioovol  25530  uniioombllem2a  25533  uniioombllem2  25534  uniioombllem3a  25535  uniioombllem3  25536  uniioombllem4  25537  uniioombllem6  25539  dyadmaxlem  25548  volivth  25558  vitalilem2  25560  vitalilem5  25563  i1frn  25628  itg2monolem1  25701  itgcnlem  25741  itgrevallem1  25746  itgreval  25748  itgle  25761  ibladd  25772  iblabslem  25779  itgspliticc  25788  itgsplitioo  25789  ditgcl  25809  ditgswap  25810  ditgsplitlem  25811  limcdif  25827  limcresi  25836  limccnp  25842  limccnp2  25843  limcco  25844  dvlip  25948  dvlip2  25950  dveq0  25955  dvgt0lem1  25957  dvivthlem1  25963  dvcnvrelem1  25972  dvcnvre  25974  dvfsumlem2  25983  dvfsumlem2OLD  25984  ftc1lem1  25992  ftc1a  25994  ftc1lem4  25996  ftc2ditglem  26002  itgsubstlem  26005  ply1rem  26121  fta1glem1  26123  ig1pdvds  26135  plyrem  26263  facth  26264  fta1lem  26265  vieta1lem1  26268  vieta1lem2  26269  aaliou3lem3  26302  aaliou3lem4  26304  aaliou3lem7  26307  taylfvallem1  26314  tayl0  26319  taylply2  26325  taylply2OLD  26326  radcnvle  26379  psercnlem2  26384  psercnlem1  26385  psercn  26386  pserdvlem1  26387  pserdvlem2  26388  abelth2  26402  coseq00topi  26461  coseq0negpitopi  26462  cosordlem  26489  tanord1  26496  efif1olem1  26501  loglesqrt  26721  logreclem  26722  relogbval  26732  nnlogbexp  26741  chordthmlem4  26795  quart1  26816  quartlem2  26818  quartlem3  26819  quartlem4  26820  quart  26821  acosbnd  26860  atancj  26870  atanlogsublem  26875  atantan  26883  atanbndlem  26885  dvatan  26895  atantayl  26897  rlimcnp2  26926  divsqrtsumlem  26940  ftalem5  27037  ftalem7  27039  basellem4  27044  basellem5  27045  perfectlem2  27191  dchrinv  27222  chpdifbndlem1  27514  pntibndlem2  27552  pntlemc  27556  pntlema  27557  pntlemb  27558  pntlemg  27559  pntlemh  27560  pntlemq  27562  pntlemr  27563  pntlemj  27564  pntlemi  27565  pntlemf  27566  pntlemk  27567  pntlemo  27568  pntleme  27569  pntlem3  27570  pntleml  27572  abvcxp  27576  scutun12  27772  slerec  27781  cofcut2  27873  cofcutr  27875  cofcutrtime  27878  cutmax  27885  cutmin  27886  addsproplem4  27922  addsproplem6  27924  addsuniflem  27951  addsasslem1  27953  addsasslem2  27954  negsproplem5  27981  negsproplem6  27982  negscut2  27989  negsunif  28004  mulsproplem12  28070  ssltmul1  28090  ssltmul2  28091  mulsuniflem  28092  precsexlem11  28158  axtgpasch  28392  cgr3simp2  28446  legso  28524  hlne2  28531  hlln  28532  mirhl  28604  inagswap  28766  inagne2  28768  dfcgrg2  28788  subumgredg2  29210  upgrres1  29238  nb3grprlem1  29305  wlkp  29542  wspthsswwlkn  29846  2wlkdlem6  29859  clwwisshclwwsn  29943  erclwwlkeqlen  29946  erclwwlksym  29948  erclwwlktr  29949  clwwlkn  29953  clwwlknwrd  29961  clwwlknonex2e  30037  grpoass  30430  vcsm  30489  nvf  30587  ssps  30657  minvecolem2  30802  minvecolem4c  30806  minvecolem4  30807  minvecolem5  30808  minvecolem6  30809  eigvec1  31889  eliccelico  32700  elicoelioo  32701  pmtrto1cl  33056  cyc3evpm  33107  slmdvsdi  33158  slmdvs1  33163  sdrgdvcl  33239  sdrginvcl  33240  fldgenssp  33258  imaslmod  33314  prmidlnr  33400  qsidomlem2  33414  mxidlnr  33425  0ringmon1p  33516  irngnzply1lem  33677  irngnzply1  33678  ply1annig1p  33684  minplycl  33686  ply1annprmidl  33687  minplym1p  33693  minplynzm1p  33694  algextdeglem1  33697  algextdeglem2  33698  algextdeglem3  33699  algextdeglem4  33700  algextdeglem5  33701  constrsqrtcl  33759  cnre2csqlem  33887  lmxrge0  33929  sigaclci  34109  difelsiga  34110  insiga  34114  ldsysgenld  34137  sigapildsyslem  34138  sigapildsys  34139  ldgenpisyslem1  34140  measvnul  34183  sibfrn  34315  eulerpartlemt  34349  eulerpartlemmf  34353  tg5segofs  34651  lpadleft  34661  spthcycl  35097  subgrwlk  35100  acycgrcycl  35115  subfacp1lem2a  35148  subfacp1lem3  35150  subfacp1lem4  35151  subfacp1lem5  35152  sconnpht2  35206  sconnpi1  35207  resconn  35214  cvmsss  35235  cvmsn0  35236  cvmlift2lem3  35273  cvmlift2lem7  35277  cvmliftphtlem  35285  cvmliftpht  35286  cvmlift3lem5  35291  cvmlift3lem6  35292  msrf  35510  elmsta  35516  mclsax  35537  mthmpps  35550  mclspps  35552  ivthALT  36299  weiunpo  36429  weiunso  36430  weiunfr  36431  weiunse  36432  poimirlem17  37607  poimirlem20  37610  ibladdnc  37647  iblabsnclem  37653  ftc1cnnclem  37661  ftc1anc  37671  ftc2nc  37672  heiborlem3  37783  iccbnd  37810  rngohom1  37938  idl0cl  37988  maxidlnr  38012  lshpne  38946  opococ  39159  opexmid  39171  hlclat  39322  lclkrslem2  41503  fzne2d  41939  dvrelog2  42023  dvrelog3  42024  0nonelalab  42026  aks4d1p1p5  42034  primrootsunit1  42056  primrootscoprmpow  42058  primrootscoprbij  42061  primrootspoweq0  42065  aks6d1c2lem3  42085  aks6d1c2  42089  aks6d1c6lem5  42136  aks5lem1  42145  aks5lem2  42146  aks5lem3a  42148  aks5lem5a  42150  unitscyglem1  42154  metakunt8  42171  metakunt21  42184  metakunt22  42185  metakunt24  42187  metakunt25  42188  evlsval3  42529  flt4lem5f  42627  flt4lem7  42629  nna4b4nsq  42630  gneispacern2  44110  cvgdvgrat  44285  iccshift  45495  iccsuble  45496  icoiccdif  45501  mullimc  45593  limccog  45597  mullimcf  45600  lptioo2  45608  limcmptdm  45612  limcicciooub  45614  xlimmnfvlem1  45809  xlimpnfvlem1  45813  icccncfext  45864  cncfioobdlem  45873  ditgeqiooicc  45937  itgsubsticc  45953  iblcncfioo  45955  itgiccshift  45957  itgperiod  45958  itgsbtaddcnst  45959  stoweidlem31  46008  stoweidlem36  46013  stoweidlem38  46015  stoweidlem44  46021  stoweidlem62  46039  dirkercncflem1  46080  dirkercncflem4  46083  fourierdlem26  46110  fourierdlem32  46116  fourierdlem33  46117  fourierdlem37  46121  fourierdlem42  46126  fourierdlem54  46137  fourierdlem63  46146  fourierdlem64  46147  fourierdlem65  46148  fourierdlem69  46152  fourierdlem74  46157  fourierdlem75  46158  fourierdlem79  46162  fourierdlem81  46164  fourierdlem82  46165  fourierdlem89  46172  fourierdlem90  46173  fourierdlem91  46174  fourierdlem93  46176  fourierdlem101  46184  fourierdlem111  46194  saldifcl  46296  unisalgen2  46331  hoidmv1lelem3  46570  smff  46709  sigardiv  46838  sigarcol  46841  sharhght  46842  sigaradd  46843  cevathlem1  46844  cevathlem2  46845  cevath  46846  proththd  47576  perfectALTVlem2  47684  gpgnbgrvtx0  48024  gpgnbgrvtx1  48025  imasubc2  49040  imaf1co  49043  idfullsubc  49048  fucofulem1  49169