Theorem simp2d 1150

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

Syntax hints:   → wi 4   ∧ w3a 1093

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 209  df-an 398  df-3an 1095

This theorem is referenced by:  simp2bi  1153  f1dom3fv3dif  7215  f1dom3el3dif  7216  f1prex  7231  oeeui  8532  resixp  8875  domssex  9070  cantnflem1a  9601  cantnflem1d  9604  cantnflem3  9607  cantnflem4  9608  fpwwe2lem6  10555  canthnumlem  10567  canthp1lem2  10572  wun0  10637  lelttrdi  11304  supmullem2  12122  supmul  12123  ixxdisj  13308  ixxun  13309  ixxss1  13311  ixxss2  13312  ixxss12  13313  ixxub  13314  ixxlb  13315  ubioo  13325  elicore  13346  iccgelb  13350  iccss2  13365  icodisj  13424  xov1plusxeqvd  13446  fldiv  13814  immul  15093  sqrtge0  15214  sqrtrege0  15323  icco1  15497  ruclem2  16194  ruclem3  16195  ruclem8  16199  ruclem12  16203  gcddvds  16467  crth  16743  phimullem  16744  eulerthlem1  16746  eulerthlem2  16747  prmreclem3  16884  sectcan  17717  sectco  17718  sectmon  17744  monsect  17745  funcixp  17829  funcsect  17834  invfuc  17939  coapm  18033  catciso  18073  posasymb  18280  ipodrsima  18502  pstr2  18532  psdmrn  18534  psref  18535  mhmlin  18756  subm0cl  18774  eqger  19148  eqgcpbl  19152  gaorber  19277  orbstafun  19280  cayleyth  19384  pmtrrn2  19429  pmtrfinv  19430  dfod2  19533  sylow2blem1  19589  dprdf  19977  dprdff  19983  dprdfcl  19984  dprdsplit  20019  dpjcntz  20023  ablfac1a  20040  ablfac1b  20041  lmodvsdi  20878  lbssp  21072  2idlcpblrng  21267  evlsval3  22068  mpff  22091  mpfaddcl  22092  mpfmulcl  22093  mpfind  22094  pf1rcl  22338  mpfpf1  22340  mdetunilem2  22599  mdetunilem5  22602  mdetunilem6  22603  chfacfisfcpmat  22841  pnfnei  23206  cnptop2  23229  lmcl  23283  lmcnp  23290  flimfil  23955  tlmlmod  24175  ustbasel  24193  ustincl  24194  ustinvel  24196  ustfilxp  24199  tusunif  24254  imasdsf1olem  24359  xmeter  24419  tmsds  24470  metustexhalf  24542  nlmlmod  24664  qdensere  24755  blcvx  24784  tgqioo  24786  icccmplem2  24810  reconnlem1  24813  cnmpopc  24916  phtpcer  24983  phtpcco2  24987  pcohtpylem  25007  pcohtpy  25008  pcophtb  25017  om1addcl  25021  pi1blem  25027  pi1cpbl  25032  pi1grplem  25037  pi1inv  25040  pi1xfrf  25041  pi1xfr  25043  pi1xfrcnvlem  25044  pi1cof  25047  pi1coghm  25049  cphnlm  25160  cphsqrtcl2  25174  tcphcph  25225  lmcau  25301  bcthlem4  25315  minveclem4c  25413  minveclem2  25414  minveclem3b  25416  minveclem4  25420  minveclem6  25422  ivthicc  25446  ovolfsval  25458  ovollb2lem  25476  ovolshftlem1  25497  ovolscalem1  25501  ovolicc1  25504  ovolicc2lem2  25506  ovolicc2lem4  25508  ovolicc2lem5  25509  ovolicopnf  25512  ioombl1lem1  25546  ioombl1lem3  25548  ioombl1lem4  25549  uniioovol  25567  uniioombllem2a  25570  uniioombllem2  25571  uniioombllem3a  25572  uniioombllem3  25573  uniioombllem4  25574  uniioombllem6  25576  dyadmaxlem  25585  volivth  25595  vitalilem2  25597  vitalilem5  25600  i1frn  25665  itg2monolem1  25738  itgcnlem  25778  itgrevallem1  25783  itgreval  25785  itgle  25798  ibladd  25809  iblabslem  25816  itgspliticc  25825  itgsplitioo  25826  ditgcl  25846  ditgswap  25847  ditgsplitlem  25848  limcdif  25864  limcresi  25873  limccnp  25879  limccnp2  25880  limcco  25881  dvlip  25981  dvlip2  25983  dveq0  25988  dvgt0lem1  25990  dvivthlem1  25996  dvcnvrelem1  26005  dvcnvre  26007  dvfsumlem2  26015  ftc1lem1  26023  ftc1a  26025  ftc1lem4  26027  ftc2ditglem  26033  itgsubstlem  26036  ply1rem  26152  fta1glem1  26154  ig1pdvds  26166  plyrem  26292  facth  26293  fta1lem  26294  vieta1lem1  26297  vieta1lem2  26298  aaliou3lem3  26331  aaliou3lem4  26333  aaliou3lem7  26336  taylfvallem1  26343  tayl0  26348  taylply2  26354  radcnvle  26406  psercnlem2  26410  psercnlem1  26411  psercn  26412  pserdvlem1  26413  pserdvlem2  26414  abelth2  26428  coseq00topi  26487  coseq0negpitopi  26488  cosordlem  26515  tanord1  26522  efif1olem1  26527  loglesqrt  26746  logreclem  26747  relogbval  26757  nnlogbexp  26766  chordthmlem4  26820  quart1  26841  quartlem2  26843  quartlem3  26844  quartlem4  26845  quart  26846  acosbnd  26885  atancj  26895  atanlogsublem  26900  atantan  26908  atanbndlem  26910  dvatan  26920  atantayl  26922  rlimcnp2  26951  divsqrtsumlem  26964  ftalem5  27061  ftalem7  27063  basellem4  27068  basellem5  27069  perfectlem2  27214  dchrinv  27245  chpdifbndlem1  27537  pntibndlem2  27575  pntlemc  27579  pntlema  27580  pntlemb  27581  pntlemg  27582  pntlemh  27583  pntlemq  27585  pntlemr  27586  pntlemj  27587  pntlemi  27588  pntlemf  27589  pntlemk  27590  pntlemo  27591  pntleme  27592  pntlem3  27593  pntleml  27595  abvcxp  27599  cutsun12  27802  lesrec  27811  eqcuts3  27816  cofcut2  27934  cofcutr  27936  cofcutrtime  27939  cutmax  27946  cutmin  27947  addsproplem4  27984  addsproplem6  27986  addsuniflem  28013  addsasslem1  28015  addsasslem2  28016  negsproplem5  28044  negsproplem6  28045  negcut2  28052  negsunif  28067  mulsproplem12  28139  sltmuls1  28159  sltmuls2  28160  mulsuniflem  28161  precsexlem11  28229  twocut  28435  pw2cut2  28474  axtgpasch  28555  cgr3simp2  28609  legso  28687  hlne2  28694  hlln  28695  mirhl  28767  inagswap  28929  inagne2  28931  dfcgrg2  28951  subumgredg2  29374  upgrres1  29402  nb3grprlem1  29469  wlkp  29705  wspthsswwlkn  30006  2wlkdlem6  30019  clwwisshclwwsn  30106  erclwwlkeqlen  30109  erclwwlksym  30111  erclwwlktr  30112  clwwlkn  30116  clwwlknwrd  30124  clwwlknonex2e  30200  grpoass  30594  vcsm  30653  nvf  30751  ssps  30821  minvecolem2  30966  minvecolem4c  30970  minvecolem4  30971  minvecolem5  30972  minvecolem6  30973  eigvec1  32053  eliccelico  32871  elicoelioo  32872  pmtrto1cl  33182  cyc3evpm  33233  slmdvsdi  33298  slmdvs1  33303  sdrgdvcl  33385  sdrginvcl  33386  fldgenssp  33404  imaslmod  33438  prmidlnr  33524  qsidomlem2  33538  mxidlnr  33549  0ringmon1p  33650  irngnzply1lem  33884  irngnzply1  33885  ply1annig1p  33898  minplycl  33900  ply1annprmidl  33901  minplym1p  33907  minplynzm1p  33908  algextdeglem1  33911  algextdeglem2  33912  algextdeglem3  33913  algextdeglem4  33914  algextdeglem5  33915  constrsqrtcl  33973  cnre2csqlem  34104  lmxrge0  34146  sigaclci  34326  difelsiga  34327  insiga  34331  ldsysgenld  34354  sigapildsyslem  34355  sigapildsys  34356  ldgenpisyslem1  34357  measvnul  34400  sibfrn  34531  eulerpartlemt  34565  eulerpartlemmf  34569  tg5segofs  34870  lpadleft  34880  spthcycl  35370  subgrwlk  35373  acycgrcycl  35388  subfacp1lem2a  35421  subfacp1lem3  35423  subfacp1lem4  35424  subfacp1lem5  35425  sconnpht2  35479  sconnpi1  35480  resconn  35487  cvmsss  35508  cvmsn0  35509  cvmlift2lem3  35546  cvmlift2lem7  35550  cvmliftphtlem  35558  cvmliftpht  35559  cvmlift3lem5  35564  cvmlift3lem6  35565  msrf  35783  elmsta  35789  mclsax  35810  mthmpps  35823  mclspps  35825  ivthALT  36576  weiunpo  36706  weiunso  36707  weiunfr  36708  weiunse  36709  poimirlem17  38017  poimirlem20  38020  ibladdnc  38057  iblabsnclem  38063  ftc1cnnclem  38071  ftc1anc  38081  ftc2nc  38082  heiborlem3  38193  iccbnd  38220  rngohom1  38348  idl0cl  38398  maxidlnr  38422  lshpne  39487  opococ  39700  opexmid  39712  hlclat  39863  lclkrslem2  42043  fzne2d  42478  dvrelog2  42562  dvrelog3  42563  0nonelalab  42565  aks4d1p1p5  42573  primrootsunit1  42595  primrootscoprmpow  42597  primrootscoprbij  42600  primrootspoweq0  42604  aks6d1c2lem3  42624  aks6d1c2  42628  aks6d1c6lem5  42675  aks5lem1  42684  aks5lem2  42685  aks5lem3a  42687  aks5lem5a  42689  unitscyglem1  42693  flt4lem5f  43120  flt4lem7  43122  nna4b4nsq  43123  gneispacern2  44596  cvgdvgrat  44770  iccshift  45975  iccsuble  45976  icoiccdif  45981  mullimc  46073  limccog  46077  mullimcf  46080  lptioo2  46088  limcmptdm  46090  limcicciooub  46092  xlimmnfvlem1  46287  xlimpnfvlem1  46291  icccncfext  46342  cncfioobdlem  46351  ditgeqiooicc  46415  itgsubsticc  46431  iblcncfioo  46433  itgiccshift  46435  itgperiod  46436  itgsbtaddcnst  46437  stoweidlem31  46486  stoweidlem36  46491  stoweidlem38  46493  stoweidlem44  46499  stoweidlem62  46517  dirkercncflem1  46558  dirkercncflem4  46561  fourierdlem26  46588  fourierdlem32  46594  fourierdlem33  46595  fourierdlem37  46599  fourierdlem42  46604  fourierdlem54  46615  fourierdlem63  46624  fourierdlem64  46625  fourierdlem65  46626  fourierdlem69  46630  fourierdlem74  46635  fourierdlem75  46636  fourierdlem79  46640  fourierdlem81  46642  fourierdlem82  46643  fourierdlem89  46650  fourierdlem90  46651  fourierdlem91  46652  fourierdlem93  46654  fourierdlem101  46662  fourierdlem111  46672  saldifcl  46774  unisalgen2  46809  hoidmv1lelem3  47048  smff  47187  sigardiv  47316  sigarcol  47319  sharhght  47320  sigaradd  47321  cevathlem1  47322  cevathlem2  47323  cevath  47324  proththd  48104  perfectALTVlem2  48225  gpgnbgrvtx0  48577  gpgnbgrvtx1  48578  imasubc2  49654  imaf1co  49657  idfullsubc  49663  fucofulem1  49812