Theorem simp2d 1140

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

Syntax hints:   → wi 4   ∧ w3a 1084

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 206  df-an 395  df-3an 1086

This theorem is referenced by:  simp2bi  1143  f1dom3fv3dif  7278  f1dom3el3dif  7279  f1prex  7293  oeeui  8623  resixp  8952  domssex  9163  cantnflem1a  9710  cantnflem1d  9713  cantnflem3  9716  cantnflem4  9717  fpwwe2lem6  10661  canthnumlem  10673  canthp1lem2  10678  wun0  10743  lelttrdi  11408  supmullem2  12218  supmul  12219  ixxdisj  13374  ixxun  13375  ixxss1  13377  ixxss2  13378  ixxss12  13379  ixxub  13380  ixxlb  13381  ubioo  13391  elicore  13411  iccgelb  13415  iccss2  13430  icodisj  13488  xov1plusxeqvd  13510  fldiv  13861  immul  15119  sqrtge0  15240  sqrtrege0  15348  icco1  15520  ruclem2  16212  ruclem3  16213  ruclem8  16217  ruclem12  16221  gcddvds  16481  crth  16750  phimullem  16751  eulerthlem1  16753  eulerthlem2  16754  prmreclem3  16890  sectcan  17741  sectco  17742  sectmon  17768  monsect  17769  funcixp  17856  funcsect  17861  invfuc  17969  coapm  18063  catciso  18103  posasymb  18314  ipodrsima  18536  pstr2  18566  psdmrn  18568  psref  18569  mhmlin  18753  subm0cl  18771  eqger  19141  eqgcpbl  19145  gaorber  19271  orbstafun  19274  cayleyth  19382  pmtrrn2  19427  pmtrfinv  19428  dfod2  19531  sylow2blem1  19587  dprdf  19975  dprdff  19981  dprdfcl  19982  dprdsplit  20017  dpjcntz  20021  ablfac1a  20038  ablfac1b  20039  lmodvsdi  20780  lbssp  20976  2idlcpblrng  21178  mpff  22072  mpfaddcl  22073  mpfmulcl  22074  mpfind  22075  pf1rcl  22293  mpfpf1  22295  mdetunilem2  22559  mdetunilem5  22562  mdetunilem6  22563  chfacfisfcpmat  22801  pnfnei  23168  cnptop2  23191  lmcl  23245  lmcnp  23252  flimfil  23917  tlmlmod  24137  ustbasel  24155  ustincl  24156  ustinvel  24158  ustfilxp  24161  tusunif  24218  imasdsf1olem  24323  xmeter  24383  tmsds  24437  metustexhalf  24509  nlmlmod  24639  qdensere  24730  blcvx  24758  tgqioo  24760  icccmplem2  24783  reconnlem1  24786  cnmpopc  24893  phtpcer  24965  phtpcco2  24970  pcohtpylem  24990  pcohtpy  24991  pcophtb  25000  om1addcl  25004  pi1blem  25010  pi1cpbl  25015  pi1grplem  25020  pi1inv  25023  pi1xfrf  25024  pi1xfr  25026  pi1xfrcnvlem  25027  pi1cof  25030  pi1coghm  25032  cphnlm  25144  cphsqrtcl2  25158  tcphcph  25209  lmcau  25285  bcthlem4  25299  minveclem4c  25397  minveclem2  25398  minveclem3b  25400  minveclem4  25404  minveclem6  25406  ivthicc  25431  ovolfsval  25443  ovollb2lem  25461  ovolshftlem1  25482  ovolscalem1  25486  ovolicc1  25489  ovolicc2lem2  25491  ovolicc2lem4  25493  ovolicc2lem5  25494  ovolicopnf  25497  ioombl1lem1  25531  ioombl1lem3  25533  ioombl1lem4  25534  uniioovol  25552  uniioombllem2a  25555  uniioombllem2  25556  uniioombllem3a  25557  uniioombllem3  25558  uniioombllem4  25559  uniioombllem6  25561  dyadmaxlem  25570  volivth  25580  vitalilem2  25582  vitalilem5  25585  i1frn  25650  itg2monolem1  25724  itgcnlem  25763  itgrevallem1  25768  itgreval  25770  itgle  25783  ibladd  25794  iblabslem  25801  itgspliticc  25810  itgsplitioo  25811  ditgcl  25831  ditgswap  25832  ditgsplitlem  25833  limcdif  25849  limcresi  25858  limccnp  25864  limccnp2  25865  limcco  25866  dvlip  25970  dvlip2  25972  dveq0  25977  dvgt0lem1  25979  dvivthlem1  25985  dvcnvrelem1  25994  dvcnvre  25996  dvfsumlem2  26005  dvfsumlem2OLD  26006  ftc1lem1  26014  ftc1a  26016  ftc1lem4  26018  ftc2ditglem  26024  itgsubstlem  26027  ply1rem  26145  fta1glem1  26147  ig1pdvds  26159  plyrem  26285  facth  26286  fta1lem  26287  vieta1lem1  26290  vieta1lem2  26291  aaliou3lem3  26324  aaliou3lem4  26326  aaliou3lem7  26329  taylfvallem1  26336  tayl0  26341  taylply2  26347  taylply2OLD  26348  radcnvle  26401  psercnlem2  26406  psercnlem1  26407  psercn  26408  pserdvlem1  26409  pserdvlem2  26410  abelth2  26424  coseq00topi  26482  coseq0negpitopi  26483  cosordlem  26509  tanord1  26516  efif1olem1  26521  loglesqrt  26738  logreclem  26739  relogbval  26749  nnlogbexp  26758  chordthmlem4  26812  quart1  26833  quartlem2  26835  quartlem3  26836  quartlem4  26837  quart  26838  acosbnd  26877  atancj  26887  atanlogsublem  26892  atantan  26900  atanbndlem  26902  dvatan  26912  atantayl  26914  rlimcnp2  26943  divsqrtsumlem  26957  ftalem5  27054  ftalem7  27056  basellem4  27061  basellem5  27062  perfectlem2  27208  dchrinv  27239  chpdifbndlem1  27531  pntibndlem2  27569  pntlemc  27573  pntlema  27574  pntlemb  27575  pntlemg  27576  pntlemh  27577  pntlemq  27579  pntlemr  27580  pntlemj  27581  pntlemi  27582  pntlemf  27583  pntlemk  27584  pntlemo  27585  pntleme  27586  pntlem3  27587  pntleml  27589  abvcxp  27593  scutun12  27789  slerec  27798  cofcut2  27888  cofcutr  27890  cofcutrtime  27893  addsproplem4  27935  addsproplem6  27937  addsuniflem  27964  addsasslem1  27966  addsasslem2  27967  negsproplem5  27990  negsproplem6  27991  negscut2  27998  negsunif  28013  mulsproplem12  28077  ssltmul1  28097  ssltmul2  28098  mulsuniflem  28099  precsexlem11  28165  axtgpasch  28343  cgr3simp2  28397  legso  28475  hlne2  28482  hlln  28483  mirhl  28555  inagswap  28717  inagne2  28719  dfcgrg2  28739  subumgredg2  29170  upgrres1  29198  nb3grprlem1  29265  wlkp  29502  wspthsswwlkn  29801  2wlkdlem6  29814  clwwisshclwwsn  29898  erclwwlkeqlen  29901  erclwwlksym  29903  erclwwlktr  29904  clwwlkn  29908  clwwlknwrd  29916  clwwlknonex2e  29992  grpoass  30385  vcsm  30444  nvf  30542  ssps  30612  minvecolem2  30757  minvecolem4c  30761  minvecolem4  30762  minvecolem5  30763  minvecolem6  30764  eigvec1  31844  eliccelico  32627  elicoelioo  32628  pmtrto1cl  32912  cyc3evpm  32963  slmdvsdi  33014  slmdvs1  33019  sdrgdvcl  33085  sdrginvcl  33086  fldgenssp  33104  imaslmod  33164  prmidlnr  33251  qsidomlem2  33265  mxidlnr  33276  0ringmon1p  33370  irngnzply1lem  33499  irngnzply1  33500  ply1annig1p  33506  minplycl  33508  ply1annprmidl  33509  minplym1p  33514  algextdeglem1  33516  algextdeglem2  33517  algextdeglem3  33518  algextdeglem4  33519  algextdeglem5  33520  cnre2csqlem  33642  lmxrge0  33684  sigaclci  33882  difelsiga  33883  insiga  33887  ldsysgenld  33910  sigapildsyslem  33911  sigapildsys  33912  ldgenpisyslem1  33913  measvnul  33956  sibfrn  34088  eulerpartlemt  34122  eulerpartlemmf  34126  tg5segofs  34436  lpadleft  34446  spthcycl  34870  subgrwlk  34873  acycgrcycl  34888  subfacp1lem2a  34921  subfacp1lem3  34923  subfacp1lem4  34924  subfacp1lem5  34925  sconnpht2  34979  sconnpi1  34980  resconn  34987  cvmsss  35008  cvmsn0  35009  cvmlift2lem3  35046  cvmlift2lem7  35050  cvmliftphtlem  35058  cvmliftpht  35059  cvmlift3lem5  35064  cvmlift3lem6  35065  msrf  35283  elmsta  35289  mclsax  35310  mthmpps  35323  mclspps  35325  ivthALT  35950  poimirlem17  37241  poimirlem20  37244  ibladdnc  37281  iblabsnclem  37287  ftc1cnnclem  37295  ftc1anc  37305  ftc2nc  37306  heiborlem3  37417  iccbnd  37444  rngohom1  37572  idl0cl  37622  maxidlnr  37646  lshpne  38584  opococ  38797  opexmid  38809  hlclat  38960  lclkrslem2  41141  fzne2d  41583  dvrelog2  41667  dvrelog3  41668  0nonelalab  41670  aks4d1p1p5  41678  primrootsunit1  41699  primrootscoprmpow  41702  primrootscoprbij  41705  primrootspoweq0  41709  aks6d1c2lem3  41729  aks6d1c2  41733  aks6d1c6lem5  41780  aks5lem1  41789  aks5lem2  41790  metakunt8  41798  metakunt21  41811  metakunt22  41812  metakunt24  41814  metakunt25  41815  evlsval3  41927  flt4lem5f  42216  flt4lem7  42218  nna4b4nsq  42219  gneispacern2  43711  cvgdvgrat  43892  iccshift  45041  iccsuble  45042  icoiccdif  45047  mullimc  45142  limccog  45146  mullimcf  45149  lptioo2  45157  limcmptdm  45161  limcicciooub  45163  xlimmnfvlem1  45358  xlimpnfvlem1  45362  icccncfext  45413  cncfioobdlem  45422  ditgeqiooicc  45486  itgsubsticc  45502  iblcncfioo  45504  itgiccshift  45506  itgperiod  45507  itgsbtaddcnst  45508  stoweidlem31  45557  stoweidlem36  45562  stoweidlem38  45564  stoweidlem44  45570  stoweidlem62  45588  dirkercncflem1  45629  dirkercncflem4  45632  fourierdlem26  45659  fourierdlem32  45665  fourierdlem33  45666  fourierdlem37  45670  fourierdlem42  45675  fourierdlem54  45686  fourierdlem63  45695  fourierdlem64  45696  fourierdlem65  45697  fourierdlem69  45701  fourierdlem74  45706  fourierdlem75  45707  fourierdlem79  45711  fourierdlem81  45713  fourierdlem82  45714  fourierdlem89  45721  fourierdlem90  45722  fourierdlem91  45723  fourierdlem93  45725  fourierdlem101  45733  fourierdlem111  45743  saldifcl  45845  unisalgen2  45880  hoidmv1lelem3  46119  smff  46258  sigardiv  46387  sigarcol  46390  sharhght  46391  sigaradd  46392  cevathlem1  46393  cevathlem2  46394  cevath  46395  proththd  47091  perfectALTVlem2  47199