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  7197  f1dom3el3dif  7198  f1prex  7213  oeeui  8512  resixp  8852  domssex  9046  cantnflem1a  9570  cantnflem1d  9573  cantnflem3  9576  cantnflem4  9577  fpwwe2lem6  10519  canthnumlem  10531  canthp1lem2  10536  wun0  10601  lelttrdi  11267  supmullem2  12085  supmul  12086  ixxdisj  13252  ixxun  13253  ixxss1  13255  ixxss2  13256  ixxss12  13257  ixxub  13258  ixxlb  13259  ubioo  13269  elicore  13290  iccgelb  13294  iccss2  13309  icodisj  13368  xov1plusxeqvd  13390  fldiv  13756  immul  15035  sqrtge0  15156  sqrtrege0  15265  icco1  15439  ruclem2  16133  ruclem3  16134  ruclem8  16138  ruclem12  16142  gcddvds  16406  crth  16681  phimullem  16682  eulerthlem1  16684  eulerthlem2  16685  prmreclem3  16822  sectcan  17654  sectco  17655  sectmon  17681  monsect  17682  funcixp  17766  funcsect  17771  invfuc  17876  coapm  17970  catciso  18010  posasymb  18217  ipodrsima  18439  pstr2  18469  psdmrn  18471  psref  18472  mhmlin  18693  subm0cl  18711  eqger  19083  eqgcpbl  19087  gaorber  19213  orbstafun  19216  cayleyth  19320  pmtrrn2  19365  pmtrfinv  19366  dfod2  19469  sylow2blem1  19525  dprdf  19913  dprdff  19919  dprdfcl  19920  dprdsplit  19955  dpjcntz  19959  ablfac1a  19976  ablfac1b  19977  lmodvsdi  20811  lbssp  21006  2idlcpblrng  21201  mpff  22032  mpfaddcl  22033  mpfmulcl  22034  mpfind  22035  pf1rcl  22257  mpfpf1  22259  mdetunilem2  22521  mdetunilem5  22524  mdetunilem6  22525  chfacfisfcpmat  22763  pnfnei  23128  cnptop2  23151  lmcl  23205  lmcnp  23212  flimfil  23877  tlmlmod  24097  ustbasel  24115  ustincl  24116  ustinvel  24118  ustfilxp  24121  tusunif  24176  imasdsf1olem  24281  xmeter  24341  tmsds  24392  metustexhalf  24464  nlmlmod  24586  qdensere  24677  blcvx  24706  tgqioo  24708  icccmplem2  24732  reconnlem1  24735  cnmpopc  24842  phtpcer  24914  phtpcco2  24919  pcohtpylem  24939  pcohtpy  24940  pcophtb  24949  om1addcl  24953  pi1blem  24959  pi1cpbl  24964  pi1grplem  24969  pi1inv  24972  pi1xfrf  24973  pi1xfr  24975  pi1xfrcnvlem  24976  pi1cof  24979  pi1coghm  24981  cphnlm  25092  cphsqrtcl2  25106  tcphcph  25157  lmcau  25233  bcthlem4  25247  minveclem4c  25345  minveclem2  25346  minveclem3b  25348  minveclem4  25352  minveclem6  25354  ivthicc  25379  ovolfsval  25391  ovollb2lem  25409  ovolshftlem1  25430  ovolscalem1  25434  ovolicc1  25437  ovolicc2lem2  25439  ovolicc2lem4  25441  ovolicc2lem5  25442  ovolicopnf  25445  ioombl1lem1  25479  ioombl1lem3  25481  ioombl1lem4  25482  uniioovol  25500  uniioombllem2a  25503  uniioombllem2  25504  uniioombllem3a  25505  uniioombllem3  25506  uniioombllem4  25507  uniioombllem6  25509  dyadmaxlem  25518  volivth  25528  vitalilem2  25530  vitalilem5  25533  i1frn  25598  itg2monolem1  25671  itgcnlem  25711  itgrevallem1  25716  itgreval  25718  itgle  25731  ibladd  25742  iblabslem  25749  itgspliticc  25758  itgsplitioo  25759  ditgcl  25779  ditgswap  25780  ditgsplitlem  25781  limcdif  25797  limcresi  25806  limccnp  25812  limccnp2  25813  limcco  25814  dvlip  25918  dvlip2  25920  dveq0  25925  dvgt0lem1  25927  dvivthlem1  25933  dvcnvrelem1  25942  dvcnvre  25944  dvfsumlem2  25953  dvfsumlem2OLD  25954  ftc1lem1  25962  ftc1a  25964  ftc1lem4  25966  ftc2ditglem  25972  itgsubstlem  25975  ply1rem  26091  fta1glem1  26093  ig1pdvds  26105  plyrem  26233  facth  26234  fta1lem  26235  vieta1lem1  26238  vieta1lem2  26239  aaliou3lem3  26272  aaliou3lem4  26274  aaliou3lem7  26277  taylfvallem1  26284  tayl0  26289  taylply2  26295  taylply2OLD  26296  radcnvle  26349  psercnlem2  26354  psercnlem1  26355  psercn  26356  pserdvlem1  26357  pserdvlem2  26358  abelth2  26372  coseq00topi  26431  coseq0negpitopi  26432  cosordlem  26459  tanord1  26466  efif1olem1  26471  loglesqrt  26691  logreclem  26692  relogbval  26702  nnlogbexp  26711  chordthmlem4  26765  quart1  26786  quartlem2  26788  quartlem3  26789  quartlem4  26790  quart  26791  acosbnd  26830  atancj  26840  atanlogsublem  26845  atantan  26853  atanbndlem  26855  dvatan  26865  atantayl  26867  rlimcnp2  26896  divsqrtsumlem  26910  ftalem5  27007  ftalem7  27009  basellem4  27014  basellem5  27015  perfectlem2  27161  dchrinv  27192  chpdifbndlem1  27484  pntibndlem2  27522  pntlemc  27526  pntlema  27527  pntlemb  27528  pntlemg  27529  pntlemh  27530  pntlemq  27532  pntlemr  27533  pntlemj  27534  pntlemi  27535  pntlemf  27536  pntlemk  27537  pntlemo  27538  pntleme  27539  pntlem3  27540  pntleml  27542  abvcxp  27546  scutun12  27744  slerec  27753  eqscut3  27758  cofcut2  27859  cofcutr  27861  cofcutrtime  27864  cutmax  27871  cutmin  27872  addsproplem4  27908  addsproplem6  27910  addsuniflem  27937  addsasslem1  27939  addsasslem2  27940  negsproplem5  27967  negsproplem6  27968  negscut2  27975  negsunif  27990  mulsproplem12  28059  ssltmul1  28079  ssltmul2  28080  mulsuniflem  28081  precsexlem11  28148  twocut  28339  pw2cut2  28375  axtgpasch  28438  cgr3simp2  28492  legso  28570  hlne2  28577  hlln  28578  mirhl  28650  inagswap  28812  inagne2  28814  dfcgrg2  28834  subumgredg2  29256  upgrres1  29284  nb3grprlem1  29351  wlkp  29588  wspthsswwlkn  29889  2wlkdlem6  29902  clwwisshclwwsn  29986  erclwwlkeqlen  29989  erclwwlksym  29991  erclwwlktr  29992  clwwlkn  29996  clwwlknwrd  30004  clwwlknonex2e  30080  grpoass  30473  vcsm  30532  nvf  30630  ssps  30700  minvecolem2  30845  minvecolem4c  30849  minvecolem4  30850  minvecolem5  30851  minvecolem6  30852  eigvec1  31932  eliccelico  32750  elicoelioo  32751  pmtrto1cl  33058  cyc3evpm  33109  slmdvsdi  33174  slmdvs1  33179  sdrgdvcl  33255  sdrginvcl  33256  fldgenssp  33274  imaslmod  33308  prmidlnr  33394  qsidomlem2  33408  mxidlnr  33419  0ringmon1p  33510  irngnzply1lem  33693  irngnzply1  33694  ply1annig1p  33707  minplycl  33709  ply1annprmidl  33710  minplym1p  33716  minplynzm1p  33717  algextdeglem1  33720  algextdeglem2  33721  algextdeglem3  33722  algextdeglem4  33723  algextdeglem5  33724  constrsqrtcl  33782  cnre2csqlem  33913  lmxrge0  33955  sigaclci  34135  difelsiga  34136  insiga  34140  ldsysgenld  34163  sigapildsyslem  34164  sigapildsys  34165  ldgenpisyslem1  34166  measvnul  34209  sibfrn  34340  eulerpartlemt  34374  eulerpartlemmf  34378  tg5segofs  34676  lpadleft  34686  spthcycl  35141  subgrwlk  35144  acycgrcycl  35159  subfacp1lem2a  35192  subfacp1lem3  35194  subfacp1lem4  35195  subfacp1lem5  35196  sconnpht2  35250  sconnpi1  35251  resconn  35258  cvmsss  35279  cvmsn0  35280  cvmlift2lem3  35317  cvmlift2lem7  35321  cvmliftphtlem  35329  cvmliftpht  35330  cvmlift3lem5  35335  cvmlift3lem6  35336  msrf  35554  elmsta  35560  mclsax  35581  mthmpps  35594  mclspps  35596  ivthALT  36348  weiunpo  36478  weiunso  36479  weiunfr  36480  weiunse  36481  poimirlem17  37656  poimirlem20  37659  ibladdnc  37696  iblabsnclem  37702  ftc1cnnclem  37710  ftc1anc  37720  ftc2nc  37721  heiborlem3  37832  iccbnd  37859  rngohom1  37987  idl0cl  38037  maxidlnr  38061  lshpne  39000  opococ  39213  opexmid  39225  hlclat  39376  lclkrslem2  41556  fzne2d  41992  dvrelog2  42076  dvrelog3  42077  0nonelalab  42079  aks4d1p1p5  42087  primrootsunit1  42109  primrootscoprmpow  42111  primrootscoprbij  42114  primrootspoweq0  42118  aks6d1c2lem3  42138  aks6d1c2  42142  aks6d1c6lem5  42189  aks5lem1  42198  aks5lem2  42199  aks5lem3a  42201  aks5lem5a  42203  unitscyglem1  42207  evlsval3  42571  flt4lem5f  42669  flt4lem7  42671  nna4b4nsq  42672  gneispacern2  44151  cvgdvgrat  44325  iccshift  45537  iccsuble  45538  icoiccdif  45543  mullimc  45635  limccog  45639  mullimcf  45642  lptioo2  45650  limcmptdm  45652  limcicciooub  45654  xlimmnfvlem1  45849  xlimpnfvlem1  45853  icccncfext  45904  cncfioobdlem  45913  ditgeqiooicc  45977  itgsubsticc  45993  iblcncfioo  45995  itgiccshift  45997  itgperiod  45998  itgsbtaddcnst  45999  stoweidlem31  46048  stoweidlem36  46053  stoweidlem38  46055  stoweidlem44  46061  stoweidlem62  46079  dirkercncflem1  46120  dirkercncflem4  46123  fourierdlem26  46150  fourierdlem32  46156  fourierdlem33  46157  fourierdlem37  46161  fourierdlem42  46166  fourierdlem54  46177  fourierdlem63  46186  fourierdlem64  46187  fourierdlem65  46188  fourierdlem69  46192  fourierdlem74  46197  fourierdlem75  46198  fourierdlem79  46202  fourierdlem81  46204  fourierdlem82  46205  fourierdlem89  46212  fourierdlem90  46213  fourierdlem91  46214  fourierdlem93  46216  fourierdlem101  46224  fourierdlem111  46234  saldifcl  46336  unisalgen2  46371  hoidmv1lelem3  46610  smff  46749  sigardiv  46878  sigarcol  46881  sharhght  46882  sigaradd  46883  cevathlem1  46884  cevathlem2  46885  cevath  46886  proththd  47624  perfectALTVlem2  47732  gpgnbgrvtx0  48084  gpgnbgrvtx1  48085  imasubc2  49163  imaf1co  49166  idfullsubc  49172  fucofulem1  49321