Theorem simp2d 1161

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

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  simp2bi  1164  f1dom3fv3dif  7273  f1dom3el3dif  7274  f1prex  7293  oeeui  8597  resixp  8940  domssex  9136  cantnflem1a  9664  cantnflem1d  9667  cantnflem3  9670  cantnflem4  9671  fpwwe2lem6  10639  canthnumlem  10651  canthp1lem2  10656  wun0  10721  lelttrdi  11390  supmullem2  12204  supmul  12205  ixxdisj  13405  ixxun  13406  ixxss1  13408  ixxss2  13409  ixxss12  13410  ixxub  13411  ixxlb  13412  ubioo  13422  elicore  13443  iccgelb  13447  iccss2  13462  icodisj  13521  xov1plusxeqvd  13543  fldiv  13913  immul  15213  sqrtge0  15334  sqrtrege0  15443  icco1  15617  ruclem2  16313  ruclem3  16314  ruclem8  16318  ruclem12  16322  gcddvds  16586  crth  16862  phimullem  16863  eulerthlem1  16865  eulerthlem2  16866  prmreclem3  17003  sectcan  17837  sectco  17838  sectmon  17864  monsect  17865  funcixp  17949  funcsect  17954  invfuc  18059  coapm  18153  catciso  18193  posasymb  18400  ipodrsima  18622  pstr2  18652  psdmrn  18654  psref  18655  mhmlin  18876  subm0cl  18894  eqger  19271  eqgcpbl  19275  gaorber  19403  orbstafun  19406  cayleyth  19510  pmtrrn2  19555  pmtrfinv  19556  dfod2  19659  sylow2blem1  19715  dprdf  20103  dprdff  20109  dprdfcl  20110  dprdsplit  20145  dpjcntz  20149  ablfac1a  20166  ablfac1b  20167  lmodvsdi  21036  lbssp  21230  2idlcpblrng  21440  prmidlnr  21494  qsidomlem2  21511  evlsval3  22270  mpff  22293  mpfaddcl  22294  mpfmulcl  22295  mpfind  22296  pf1rcl  22539  mpfpf1  22541  mdetunilem2  22800  mdetunilem5  22803  mdetunilem6  22804  chfacfisfcpmat  23042  pnfnei  23407  cnptop2  23430  lmcl  23484  lmcnp  23491  flimfil  24156  tlmlmod  24376  ustbasel  24394  ustincl  24395  ustinvel  24397  ustfilxp  24400  tusunif  24455  imasdsf1olem  24560  xmeter  24620  tmsds  24671  metustexhalf  24743  nlmlmod  24865  qdensere  24956  blcvx  24985  tgqioo  24987  icccmplem2  25011  reconnlem1  25014  cnmpopc  25117  phtpcer  25184  phtpcco2  25188  pcohtpylem  25208  pcohtpy  25209  pcophtb  25218  om1addcl  25222  pi1blem  25228  pi1cpbl  25233  pi1grplem  25238  pi1inv  25241  pi1xfrf  25242  pi1xfr  25244  pi1xfrcnvlem  25245  pi1cof  25248  pi1coghm  25250  cphnlm  25361  cphsqrtcl2  25375  tcphcph  25426  lmcau  25502  bcthlem4  25516  minveclem4c  25614  minveclem2  25615  minveclem3b  25617  minveclem4  25621  minveclem6  25623  ivthicc  25647  ovolfsval  25659  ovollb2lem  25677  ovolshftlem1  25698  ovolscalem1  25702  ovolicc1  25705  ovolicc2lem2  25707  ovolicc2lem4  25709  ovolicc2lem5  25710  ovolicopnf  25713  ioombl1lem1  25747  ioombl1lem3  25749  ioombl1lem4  25750  uniioovol  25768  uniioombllem2a  25771  uniioombllem2  25772  uniioombllem3a  25773  uniioombllem3  25774  uniioombllem4  25775  uniioombllem6  25777  dyadmaxlem  25786  volivth  25796  vitalilem2  25798  vitalilem5  25801  i1frn  25866  itg2monolem1  25939  itgcnlem  25979  itgrevallem1  25984  itgreval  25986  itgle  25999  ibladd  26010  iblabslem  26017  itgspliticc  26026  itgsplitioo  26027  ditgcl  26047  ditgswap  26048  ditgsplitlem  26049  limcdif  26065  limcresi  26074  limccnp  26080  limccnp2  26081  limcco  26082  dvlip  26182  dvlip2  26184  dveq0  26189  dvgt0lem1  26191  dvivthlem1  26197  dvcnvrelem1  26206  dvcnvre  26208  dvfsumlem2  26216  ftc1lem1  26224  ftc1a  26226  ftc1lem4  26228  ftc2ditglem  26234  itgsubstlem  26237  ply1rem  26353  fta1glem1  26355  ig1pdvds  26367  plyrem  26496  facth  26497  fta1lem  26498  vieta1lem1  26501  vieta1lem2  26502  aaliou3lem3  26537  aaliou3lem4  26539  aaliou3lem7  26542  taylfvallem1  26550  tayl0  26555  taylply2  26561  radcnvle  26613  psercnlem2  26617  psercnlem1  26618  psercn  26619  pserdvlem1  26620  pserdvlem2  26621  abelth2  26635  coseq00topi  26697  coseq0negpitopi  26698  cosordlem  26725  tanord1  26732  efif1olem1  26737  loglesqrt  26956  logreclem  26957  relogbval  26967  nnlogbexp  26976  chordthmlem4  27030  quart1  27051  quartlem2  27053  quartlem3  27054  quartlem4  27055  quart  27056  acosbnd  27095  atancj  27105  atanlogsublem  27110  atantan  27118  atanbndlem  27120  dvatan  27130  atantayl  27132  rlimcnp2  27161  divsqrtsumlem  27174  ftalem5  27271  ftalem7  27273  basellem4  27278  basellem5  27279  perfectlem2  27424  dchrinv  27455  chpdifbndlem1  27747  pntibndlem2  27785  pntlemc  27789  pntlema  27790  pntlemb  27791  pntlemg  27792  pntlemh  27793  pntlemq  27795  pntlemr  27796  pntlemj  27797  pntlemi  27798  pntlemf  27799  pntlemk  27800  pntlemo  27801  pntleme  27802  pntlem3  27803  pntleml  27805  abvcxp  27809  cutsun12  28013  lesrec  28022  eqcuts3  28027  cofcut2  28145  cofcutr  28147  cofcutrtime  28150  cutmax  28157  cutmin  28158  addsproplem4  28195  addsproplem6  28197  addsuniflem  28224  addsasslem1  28226  addsasslem2  28227  negsproplem5  28255  negsproplem6  28256  negcut2  28263  negsunif  28278  mulsproplem12  28350  sltmuls1  28370  sltmuls2  28371  mulsuniflem  28372  precsexlem11  28440  twocut  28646  pw2cut2  28685  axtgpasch  28766  cgr3simp2  28820  legso  28898  hlne2  28908  hlln  28909  mirhl  28986  inagswap  29188  inagne2  29190  dfcgrg2  29210  subumgredg2  29665  upgrres1  29693  nb3grprlem1  29760  wlkp  29996  wspthsswwlkn  30297  2wlkdlem6  30310  clwwisshclwwsn  30397  erclwwlkeqlen  30400  erclwwlksym  30402  erclwwlktr  30403  clwwlkn  30407  clwwlknwrd  30415  clwwlknonex2e  30491  grpoass  30885  vcsm  30944  nvf  31042  ssps  31112  minvecolem2  31257  minvecolem4c  31261  minvecolem4  31262  minvecolem5  31263  minvecolem6  31264  eigvec1  32344  eliccelico  33152  elicoelioo  33153  pmtrto1cl  33443  cyc3evpm  33494  slmdvsdi  33559  slmdvs1  33564  sdrgdvcl  33644  sdrginvcl  33645  fldgenssp  33663  imaslmod  33697  mxidlnr  33771  0ringmon1p  33871  irngnzply1lem  34104  irngnzply1  34105  ply1annig1p  34118  minplycl  34120  ply1annprmidl  34121  minplym1p  34127  minplynzm1p  34128  algextdeglem1  34131  algextdeglem2  34132  algextdeglem3  34133  algextdeglem4  34134  algextdeglem5  34135  constrsqrtcl  34193  cnre2csqlem  34324  lmxrge0  34366  sigaclci  34546  difelsiga  34547  insiga  34551  ldsysgenld  34574  sigapildsyslem  34575  sigapildsys  34576  ldgenpisyslem1  34577  measvnul  34620  sibfrn  34751  eulerpartlemt  34785  eulerpartlemmf  34789  tg5segofs  35087  lpadleft  35097  spthcycl  35634  subgrwlk  35637  acycgrcycl  35652  subfacp1lem2a  35685  subfacp1lem3  35687  subfacp1lem4  35688  subfacp1lem5  35689  sconnpht2  35743  sconnpi1  35744  resconn  35751  cvmsss  35772  cvmsn0  35773  cvmlift2lem3  35810  cvmlift2lem7  35814  cvmliftphtlem  35822  cvmliftpht  35823  cvmlift3lem5  35828  cvmlift3lem6  35829  msrf  36047  elmsta  36053  mclsax  36074  mthmpps  36087  mclspps  36089  ivthALT  36879  weiunpo  37009  weiunso  37010  weiunfr  37011  weiunse  37012  poimirlem17  38321  poimirlem20  38324  ibladdnc  38361  iblabsnclem  38367  ftc1cnnclem  38375  ftc1anc  38385  ftc2nc  38386  heiborlem3  38497  iccbnd  38524  rngohom1  38652  idl0cl  38702  maxidlnr  38726  lshpne  39789  opococ  40002  opexmid  40014  hlclat  40165  lclkrslem2  42345  fzne2d  42780  dvrelog2  42864  dvrelog3  42865  0nonelalab  42867  aks4d1p1p5  42875  primrootsunit1  42897  primrootscoprmpow  42899  primrootscoprbij  42902  primrootspoweq0  42906  aks6d1c2lem3  42926  aks6d1c2  42930  aks6d1c6lem5  42977  aks5lem1  42986  aks5lem2  42987  aks5lem3a  42989  aks5lem5a  42991  unitscyglem1  42995  flt4lem5f  43422  flt4lem7  43424  nna4b4nsq  43425  gneispacern2  44898  cvgdvgrat  45056  iccshift  46267  iccsuble  46268  icoiccdif  46273  mullimc  46365  limccog  46369  mullimcf  46372  lptioo2  46380  limcmptdm  46382  limcicciooub  46384  xlimmnfvlem1  46579  xlimpnfvlem1  46583  icccncfext  46634  cncfioobdlem  46643  ditgeqiooicc  46707  itgsubsticc  46723  iblcncfioo  46725  itgiccshift  46727  itgperiod  46728  itgsbtaddcnst  46729  stoweidlem31  46778  stoweidlem36  46783  stoweidlem38  46785  stoweidlem44  46791  stoweidlem62  46809  dirkercncflem1  46850  dirkercncflem4  46853  fourierdlem26  46880  fourierdlem32  46886  fourierdlem33  46887  fourierdlem37  46891  fourierdlem42  46896  fourierdlem54  46907  fourierdlem63  46916  fourierdlem64  46917  fourierdlem65  46918  fourierdlem69  46922  fourierdlem74  46927  fourierdlem75  46928  fourierdlem79  46932  fourierdlem81  46934  fourierdlem82  46935  fourierdlem89  46942  fourierdlem90  46943  fourierdlem91  46944  fourierdlem93  46946  fourierdlem101  46954  fourierdlem111  46964  saldifcl  47066  unisalgen2  47101  hoidmv1lelem3  47340  smff  47479  sigardiv  47608  sigarcol  47611  sharhght  47612  sigaradd  47613  cevathlem1  47614  cevathlem2  47615  cevath  47616  proththd  48399  perfectALTVlem2  48520  gpgnbgrvtx0  48872  gpgnbgrvtx1  48873  imasubc2  49963  imaf1co  49966  idfullsubc  49972  fucofulem1  50121