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  7269  f1dom3el3dif  7270  f1prex  7289  oeeui  8594  resixp  8944  domssex  9140  cantnflem1a  9668  cantnflem1d  9671  cantnflem3  9674  cantnflem4  9675  fpwwe2lem6  10649  canthnumlem  10661  canthp1lem2  10666  wun0  10731  lelttrdi  11400  supmullem2  12214  supmul  12215  ixxdisj  13417  ixxun  13418  ixxss1  13420  ixxss2  13421  ixxss12  13422  ixxub  13423  ixxlb  13424  ubioo  13434  elicore  13455  iccgelb  13459  iccss2  13474  icodisj  13533  xov1plusxeqvd  13555  fldiv  13925  immul  15227  sqrtge0  15348  sqrtrege0  15457  icco1  15631  ruclem2  16326  ruclem3  16327  ruclem8  16331  ruclem12  16335  gcddvds  16599  crth  16875  phimullem  16876  eulerthlem1  16878  eulerthlem2  16879  prmreclem3  17016  sectcan  17850  sectco  17851  sectmon  17877  monsect  17878  funcixp  17962  funcsect  17967  invfuc  18072  coapm  18166  catciso  18206  posasymb  18413  ipodrsima  18635  pstr2  18665  psdmrn  18667  psref  18668  mhmlin  18907  subm0cl  18925  eqger  19309  eqgcpbl  19313  gaorber  19441  orbstafun  19444  cayleyth  19548  pmtrrn2  19593  pmtrfinv  19594  dfod2  19697  sylow2blem1  19753  dprdf  20141  dprdff  20147  dprdfcl  20148  dprdsplit  20183  dpjcntz  20187  ablfac1a  20204  ablfac1b  20205  lmodvsdi  21075  lbssp  21269  2idlcpblrng  21479  prmidlnr  21533  qsidomlem2  21550  evlsval3  22311  mpff  22334  mpfaddcl  22335  mpfmulcl  22336  mpfind  22337  pf1rcl  22580  mpfpf1  22582  mdetunilem2  22841  mdetunilem5  22844  mdetunilem6  22845  chfacfisfcpmat  23086  pnfnei  23451  cnptop2  23474  lmcl  23528  lmcnp  23535  flimfil  24201  tlmlmod  24421  ustbasel  24439  ustincl  24440  ustinvel  24442  ustfilxp  24445  tusunif  24500  imasdsf1olem  24605  xmeter  24665  tmsds  24716  metustexhalf  24788  nlmlmod  24910  qdensere  25001  blcvx  25030  tgqioo  25032  icccmplem2  25056  reconnlem1  25059  cnmpopc  25162  phtpcer  25229  phtpcco2  25233  pcohtpylem  25253  pcohtpy  25254  pcophtb  25263  om1addcl  25267  pi1blem  25273  pi1cpbl  25278  pi1grplem  25283  pi1inv  25286  pi1xfrf  25287  pi1xfr  25289  pi1xfrcnvlem  25290  pi1cof  25293  pi1coghm  25295  cphnlm  25406  cphsqrtcl2  25420  tcphcph  25471  lmcau  25547  bcthlem4  25561  minveclem4c  25659  minveclem2  25660  minveclem3b  25662  minveclem4  25666  minveclem6  25668  ivthicc  25692  ovolfsval  25704  ovollb2lem  25722  ovolshftlem1  25743  ovolscalem1  25747  ovolicc1  25750  ovolicc2lem2  25752  ovolicc2lem4  25754  ovolicc2lem5  25755  ovolicopnf  25758  ioombl1lem1  25792  ioombl1lem3  25794  ioombl1lem4  25795  uniioovol  25813  uniioombllem2a  25816  uniioombllem2  25817  uniioombllem3a  25818  uniioombllem3  25819  uniioombllem4  25820  uniioombllem6  25822  dyadmaxlem  25831  volivth  25841  vitalilem2  25843  vitalilem5  25846  i1frn  25911  itg2monolem1  25984  itgcnlem  26024  itgrevallem1  26029  itgreval  26031  itgle  26044  ibladd  26055  iblabslem  26062  itgspliticc  26071  itgsplitioo  26072  ditgcl  26092  ditgswap  26093  ditgsplitlem  26094  limcdif  26110  limcresi  26119  limccnp  26125  limccnp2  26126  limcco  26127  dvlip  26227  dvlip2  26229  dveq0  26234  dvgt0lem1  26236  dvivthlem1  26242  dvcnvrelem1  26251  dvcnvre  26253  dvfsumlem2  26261  ftc1lem1  26269  ftc1a  26271  ftc1lem4  26273  ftc2ditglem  26279  itgsubstlem  26282  ply1rem  26398  fta1glem1  26400  ig1pdvds  26412  plyrem  26542  facth  26543  fta1lem  26544  vieta1lem1  26549  vieta1lem2  26550  aaliou3lem3  26587  aaliou3lem4  26589  aaliou3lem7  26592  taylfvallem1  26600  tayl0  26605  taylply2  26611  radcnvle  26663  psercnlem2  26667  psercnlem1  26668  psercn  26669  pserdvlem1  26670  pserdvlem2  26671  abelth2  26685  coseq00topi  26747  coseq0negpitopi  26748  cosordlem  26775  tanord1  26782  efif1olem1  26787  loglesqrt  27006  logreclem  27007  relogbval  27017  nnlogbexp  27026  chordthmlem4  27080  quart1  27101  quartlem2  27103  quartlem3  27104  quartlem4  27105  quart  27106  acosbnd  27145  atancj  27155  atanlogsublem  27160  atantan  27168  atanbndlem  27170  dvatan  27180  atantayl  27182  rlimcnp2  27211  divsqrtsumlem  27224  ftalem5  27321  ftalem7  27323  basellem4  27328  basellem5  27329  perfectlem2  27474  dchrinv  27505  chpdifbndlem1  27797  pntibndlem2  27835  pntlemc  27839  pntlema  27840  pntlemb  27841  pntlemg  27842  pntlemh  27843  pntlemq  27845  pntlemr  27846  pntlemj  27847  pntlemi  27848  pntlemf  27849  pntlemk  27850  pntlemo  27851  pntleme  27852  pntlem3  27853  pntleml  27855  abvcxp  27859  cutsun12  28063  lesrec  28072  eqcuts3  28077  cofcut2  28195  cofcutr  28197  cofcutrtime  28200  cutmax  28207  cutmin  28208  addsproplem4  28245  addsproplem6  28247  addsuniflem  28274  addsasslem1  28276  addsasslem2  28277  negsproplem5  28305  negsproplem6  28306  negcut2  28313  negsunif  28328  mulsproplem12  28400  sltmuls1  28420  sltmuls2  28421  mulsuniflem  28422  precsexlem11  28490  twocut  28696  pw2cut2  28735  axtgpasch  28816  cgr3simp2  28871  legso  28949  hlne2  28959  hlln  28960  mirhl  29038  inagswap  29247  inagne2  29249  dfcgrg2  29295  subumgredg2  29753  upgrres1  29781  nb3grprlem1  29848  wlkp  30084  subgrwlk  30156  spthcycl  30279  wspthsswwlkn  30394  2wlkdlem6  30407  clwwisshclwwsn  30494  erclwwlkeqlen  30497  erclwwlksym  30499  erclwwlktr  30500  clwwlkn  30504  clwwlknwrd  30512  clwwlknonex2e  30588  acycgrcycl  30640  grpoass  30992  vcsm  31051  nvf  31149  ssps  31219  minvecolem2  31364  minvecolem4c  31368  minvecolem4  31369  minvecolem5  31370  minvecolem6  31371  eigvec1  32451  eliccelico  33256  elicoelioo  33257  pmtrto1cl  33547  cyc3evpm  33598  slmdvsdi  33663  slmdvs1  33668  sdrgdvcl  33748  sdrginvcl  33749  fldgenssp  33767  imaslmod  33801  mxidlnr  33875  0ringmon1p  33975  irngnzply1lem  34208  irngnzply1  34209  ply1annig1p  34222  minplycl  34224  ply1annprmidl  34225  minplym1p  34231  minplynzm1p  34232  algextdeglem1  34235  algextdeglem2  34236  algextdeglem3  34237  algextdeglem4  34238  algextdeglem5  34239  constrsqrtcl  34297  cnre2csqlem  34428  lmxrge0  34470  sigaclci  34650  difunielsiga  34651  insiga  34656  ldsysgenld  34679  sigapildsyslem  34680  sigapildsys  34681  ldgenpisyslem1  34682  measvnul  34725  sibfrn  34856  eulerpartlemt  34890  eulerpartlemmf  34894  tg5segofs  35192  lpadleft  35202  subfacp1lem2a  35767  subfacp1lem3  35769  subfacp1lem4  35770  subfacp1lem5  35771  sconnpht2  35825  sconnpi1  35826  resconn  35833  cvmsss  35854  cvmsn0  35855  cvmlift2lem3  35892  cvmlift2lem7  35896  cvmliftphtlem  35904  cvmliftpht  35905  cvmlift3lem5  35910  cvmlift3lem6  35911  msrf  36129  elmsta  36135  mclsax  36156  mthmpps  36169  mclspps  36171  ivthALT  36962  weiunpo  37092  weiunso  37093  weiunfr  37094  weiunse  37095  poimirlem17  38394  poimirlem20  38397  ibladdnc  38434  iblabsnclem  38440  ftc1cnnclem  38448  ftc1anc  38458  ftc2nc  38459  heiborlem3  38571  iccbnd  38598  rngohom1  38726  idl0cl  38776  maxidlnr  38800  lshpne  39863  opococ  40076  opexmid  40088  hlclat  40239  lclkrslem2  42419  fzne2d  42854  dvrelog2  42938  dvrelog3  42939  0nonelalab  42941  aks4d1p1p5  42949  primrootsunit1  42971  primrootscoprmpow  42973  primrootscoprbij  42976  primrootspoweq0  42980  aks6d1c2lem3  43000  aks6d1c2  43004  aks6d1c6lem5  43051  aks5lem1  43060  aks5lem2  43061  aks5lem3a  43063  aks5lem5a  43065  unitscyglem1  43069  flt4lem5f  43511  flt4lem7  43513  nna4b4nsq  43514  gneispacern2  44987  cvgdvgrat  45145  iccshift  46356  iccsuble  46357  icoiccdif  46362  mullimc  46454  limccog  46458  mullimcf  46461  lptioo2  46469  limcmptdm  46471  limcicciooub  46473  xlimmnfvlem1  46668  xlimpnfvlem1  46672  icccncfext  46723  cncfioobdlem  46732  ditgeqiooicc  46796  itgsubsticc  46812  iblcncfioo  46814  itgiccshift  46816  itgperiod  46817  itgsbtaddcnst  46818  stoweidlem31  46867  stoweidlem36  46872  stoweidlem38  46874  stoweidlem44  46880  stoweidlem62  46898  dirkercncflem1  46939  dirkercncflem4  46942  fourierdlem26  46969  fourierdlem32  46975  fourierdlem33  46976  fourierdlem37  46980  fourierdlem42  46985  fourierdlem54  46996  fourierdlem63  47005  fourierdlem64  47006  fourierdlem65  47007  fourierdlem69  47011  fourierdlem74  47016  fourierdlem75  47017  fourierdlem79  47021  fourierdlem81  47023  fourierdlem82  47024  fourierdlem89  47031  fourierdlem90  47032  fourierdlem91  47033  fourierdlem93  47035  fourierdlem101  47043  fourierdlem111  47053  saldifcl  47155  unisalgen2  47190  hoidmv1lelem3  47429  smff  47568  sigardiv  47697  sigarcol  47700  sharhght  47701  sigaradd  47702  cevathlem1  47703  cevathlem2  47704  cevath  47705  proththd  48525  perfectALTVlem2  48646  gpgnbgrvtx0  48998  gpgnbgrvtx1  48999  imasubc2  50086  imaf1co  50089  idfullsubc  50095  fucofulem1  50244  rr3fv2cld  50789