Theorem simp2d 1144

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

Syntax hints:   → wi 4   ∧ w3a 1087

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 1089

This theorem is referenced by:  simp2bi  1147  f1dom3fv3dif  7224  f1dom3el3dif  7225  f1prex  7240  oeeui  8540  resixp  8883  domssex  9078  cantnflem1a  9606  cantnflem1d  9609  cantnflem3  9612  cantnflem4  9613  fpwwe2lem6  10559  canthnumlem  10571  canthp1lem2  10576  wun0  10641  lelttrdi  11307  supmullem2  12125  supmul  12126  ixxdisj  13288  ixxun  13289  ixxss1  13291  ixxss2  13292  ixxss12  13293  ixxub  13294  ixxlb  13295  ubioo  13305  elicore  13326  iccgelb  13330  iccss2  13345  icodisj  13404  xov1plusxeqvd  13426  fldiv  13792  immul  15071  sqrtge0  15192  sqrtrege0  15301  icco1  15475  ruclem2  16169  ruclem3  16170  ruclem8  16174  ruclem12  16178  gcddvds  16442  crth  16717  phimullem  16718  eulerthlem1  16720  eulerthlem2  16721  prmreclem3  16858  sectcan  17691  sectco  17692  sectmon  17718  monsect  17719  funcixp  17803  funcsect  17808  invfuc  17913  coapm  18007  catciso  18047  posasymb  18254  ipodrsima  18476  pstr2  18506  psdmrn  18508  psref  18509  mhmlin  18730  subm0cl  18748  eqger  19119  eqgcpbl  19123  gaorber  19249  orbstafun  19252  cayleyth  19356  pmtrrn2  19401  pmtrfinv  19402  dfod2  19505  sylow2blem1  19561  dprdf  19949  dprdff  19955  dprdfcl  19956  dprdsplit  19991  dpjcntz  19995  ablfac1a  20012  ablfac1b  20013  lmodvsdi  20848  lbssp  21043  2idlcpblrng  21238  evlsval3  22056  mpff  22079  mpfaddcl  22080  mpfmulcl  22081  mpfind  22082  pf1rcl  22305  mpfpf1  22307  mdetunilem2  22569  mdetunilem5  22572  mdetunilem6  22573  chfacfisfcpmat  22811  pnfnei  23176  cnptop2  23199  lmcl  23253  lmcnp  23260  flimfil  23925  tlmlmod  24145  ustbasel  24163  ustincl  24164  ustinvel  24166  ustfilxp  24169  tusunif  24224  imasdsf1olem  24329  xmeter  24389  tmsds  24440  metustexhalf  24512  nlmlmod  24634  qdensere  24725  blcvx  24754  tgqioo  24756  icccmplem2  24780  reconnlem1  24783  cnmpopc  24890  phtpcer  24962  phtpcco2  24967  pcohtpylem  24987  pcohtpy  24988  pcophtb  24997  om1addcl  25001  pi1blem  25007  pi1cpbl  25012  pi1grplem  25017  pi1inv  25020  pi1xfrf  25021  pi1xfr  25023  pi1xfrcnvlem  25024  pi1cof  25027  pi1coghm  25029  cphnlm  25140  cphsqrtcl2  25154  tcphcph  25205  lmcau  25281  bcthlem4  25295  minveclem4c  25393  minveclem2  25394  minveclem3b  25396  minveclem4  25400  minveclem6  25402  ivthicc  25427  ovolfsval  25439  ovollb2lem  25457  ovolshftlem1  25478  ovolscalem1  25482  ovolicc1  25485  ovolicc2lem2  25487  ovolicc2lem4  25489  ovolicc2lem5  25490  ovolicopnf  25493  ioombl1lem1  25527  ioombl1lem3  25529  ioombl1lem4  25530  uniioovol  25548  uniioombllem2a  25551  uniioombllem2  25552  uniioombllem3a  25553  uniioombllem3  25554  uniioombllem4  25555  uniioombllem6  25557  dyadmaxlem  25566  volivth  25576  vitalilem2  25578  vitalilem5  25581  i1frn  25646  itg2monolem1  25719  itgcnlem  25759  itgrevallem1  25764  itgreval  25766  itgle  25779  ibladd  25790  iblabslem  25797  itgspliticc  25806  itgsplitioo  25807  ditgcl  25827  ditgswap  25828  ditgsplitlem  25829  limcdif  25845  limcresi  25854  limccnp  25860  limccnp2  25861  limcco  25862  dvlip  25966  dvlip2  25968  dveq0  25973  dvgt0lem1  25975  dvivthlem1  25981  dvcnvrelem1  25990  dvcnvre  25992  dvfsumlem2  26001  dvfsumlem2OLD  26002  ftc1lem1  26010  ftc1a  26012  ftc1lem4  26014  ftc2ditglem  26020  itgsubstlem  26023  ply1rem  26139  fta1glem1  26141  ig1pdvds  26153  plyrem  26281  facth  26282  fta1lem  26283  vieta1lem1  26286  vieta1lem2  26287  aaliou3lem3  26320  aaliou3lem4  26322  aaliou3lem7  26325  taylfvallem1  26332  tayl0  26337  taylply2  26343  taylply2OLD  26344  radcnvle  26397  psercnlem2  26402  psercnlem1  26403  psercn  26404  pserdvlem1  26405  pserdvlem2  26406  abelth2  26420  coseq00topi  26479  coseq0negpitopi  26480  cosordlem  26507  tanord1  26514  efif1olem1  26519  loglesqrt  26739  logreclem  26740  relogbval  26750  nnlogbexp  26759  chordthmlem4  26813  quart1  26834  quartlem2  26836  quartlem3  26837  quartlem4  26838  quart  26839  acosbnd  26878  atancj  26888  atanlogsublem  26893  atantan  26901  atanbndlem  26903  dvatan  26913  atantayl  26915  rlimcnp2  26944  divsqrtsumlem  26958  ftalem5  27055  ftalem7  27057  basellem4  27062  basellem5  27063  perfectlem2  27209  dchrinv  27240  chpdifbndlem1  27532  pntibndlem2  27570  pntlemc  27574  pntlema  27575  pntlemb  27576  pntlemg  27577  pntlemh  27578  pntlemq  27580  pntlemr  27581  pntlemj  27582  pntlemi  27583  pntlemf  27584  pntlemk  27585  pntlemo  27586  pntleme  27587  pntlem3  27588  pntleml  27590  abvcxp  27594  cutsun12  27798  lesrec  27807  eqcuts3  27812  cofcut2  27930  cofcutr  27932  cofcutrtime  27935  cutmax  27942  cutmin  27943  addsproplem4  27980  addsproplem6  27982  addsuniflem  28009  addsasslem1  28011  addsasslem2  28012  negsproplem5  28040  negsproplem6  28041  negcut2  28048  negsunif  28063  mulsproplem12  28135  sltmuls1  28155  sltmuls2  28156  mulsuniflem  28157  precsexlem11  28225  twocut  28431  pw2cut2  28470  axtgpasch  28551  cgr3simp2  28605  legso  28683  hlne2  28690  hlln  28691  mirhl  28763  inagswap  28925  inagne2  28927  dfcgrg2  28947  subumgredg2  29370  upgrres1  29398  nb3grprlem1  29465  wlkp  29702  wspthsswwlkn  30003  2wlkdlem6  30016  clwwisshclwwsn  30103  erclwwlkeqlen  30106  erclwwlksym  30108  erclwwlktr  30109  clwwlkn  30113  clwwlknwrd  30121  clwwlknonex2e  30197  grpoass  30590  vcsm  30649  nvf  30747  ssps  30817  minvecolem2  30962  minvecolem4c  30966  minvecolem4  30967  minvecolem5  30968  minvecolem6  30969  eigvec1  32049  eliccelico  32867  elicoelioo  32868  pmtrto1cl  33192  cyc3evpm  33243  slmdvsdi  33308  slmdvs1  33313  sdrgdvcl  33392  sdrginvcl  33393  fldgenssp  33411  imaslmod  33445  prmidlnr  33531  qsidomlem2  33545  mxidlnr  33556  0ringmon1p  33649  irngnzply1lem  33867  irngnzply1  33868  ply1annig1p  33881  minplycl  33883  ply1annprmidl  33884  minplym1p  33890  minplynzm1p  33891  algextdeglem1  33894  algextdeglem2  33895  algextdeglem3  33896  algextdeglem4  33897  algextdeglem5  33898  constrsqrtcl  33956  cnre2csqlem  34087  lmxrge0  34129  sigaclci  34309  difelsiga  34310  insiga  34314  ldsysgenld  34337  sigapildsyslem  34338  sigapildsys  34339  ldgenpisyslem1  34340  measvnul  34383  sibfrn  34514  eulerpartlemt  34548  eulerpartlemmf  34552  tg5segofs  34850  lpadleft  34860  spthcycl  35342  subgrwlk  35345  acycgrcycl  35360  subfacp1lem2a  35393  subfacp1lem3  35395  subfacp1lem4  35396  subfacp1lem5  35397  sconnpht2  35451  sconnpi1  35452  resconn  35459  cvmsss  35480  cvmsn0  35481  cvmlift2lem3  35518  cvmlift2lem7  35522  cvmliftphtlem  35530  cvmliftpht  35531  cvmlift3lem5  35536  cvmlift3lem6  35537  msrf  35755  elmsta  35761  mclsax  35782  mthmpps  35795  mclspps  35797  ivthALT  36548  weiunpo  36678  weiunso  36679  weiunfr  36680  weiunse  36681  poimirlem17  37877  poimirlem20  37880  ibladdnc  37917  iblabsnclem  37923  ftc1cnnclem  37931  ftc1anc  37941  ftc2nc  37942  heiborlem3  38053  iccbnd  38080  rngohom1  38208  idl0cl  38258  maxidlnr  38282  lshpne  39347  opococ  39560  opexmid  39572  hlclat  39723  lclkrslem2  41903  fzne2d  42339  dvrelog2  42423  dvrelog3  42424  0nonelalab  42426  aks4d1p1p5  42434  primrootsunit1  42456  primrootscoprmpow  42458  primrootscoprbij  42461  primrootspoweq0  42465  aks6d1c2lem3  42485  aks6d1c2  42489  aks6d1c6lem5  42536  aks5lem1  42545  aks5lem2  42546  aks5lem3a  42548  aks5lem5a  42550  unitscyglem1  42554  flt4lem5f  43004  flt4lem7  43006  nna4b4nsq  43007  gneispacern2  44484  cvgdvgrat  44658  iccshift  45867  iccsuble  45868  icoiccdif  45873  mullimc  45965  limccog  45969  mullimcf  45972  lptioo2  45980  limcmptdm  45982  limcicciooub  45984  xlimmnfvlem1  46179  xlimpnfvlem1  46183  icccncfext  46234  cncfioobdlem  46243  ditgeqiooicc  46307  itgsubsticc  46323  iblcncfioo  46325  itgiccshift  46327  itgperiod  46328  itgsbtaddcnst  46329  stoweidlem31  46378  stoweidlem36  46383  stoweidlem38  46385  stoweidlem44  46391  stoweidlem62  46409  dirkercncflem1  46450  dirkercncflem4  46453  fourierdlem26  46480  fourierdlem32  46486  fourierdlem33  46487  fourierdlem37  46491  fourierdlem42  46496  fourierdlem54  46507  fourierdlem63  46516  fourierdlem64  46517  fourierdlem65  46518  fourierdlem69  46522  fourierdlem74  46527  fourierdlem75  46528  fourierdlem79  46532  fourierdlem81  46534  fourierdlem82  46535  fourierdlem89  46542  fourierdlem90  46543  fourierdlem91  46544  fourierdlem93  46546  fourierdlem101  46554  fourierdlem111  46564  saldifcl  46666  unisalgen2  46701  hoidmv1lelem3  46940  smff  47079  sigardiv  47208  sigarcol  47211  sharhght  47212  sigaradd  47213  cevathlem1  47214  cevathlem2  47215  cevath  47216  proththd  47963  perfectALTVlem2  48071  gpgnbgrvtx0  48423  gpgnbgrvtx1  48424  imasubc2  49500  imaf1co  49503  idfullsubc  49509  fucofulem1  49658