Theorem simp2d 1159

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

Syntax hints:   → wi 4   ∧ w3a 1101

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 210  df-an 401  df-3an 1103

This theorem is referenced by:  simp2bi  1162  f1dom3fv3dif  7266  f1dom3el3dif  7267  f1prex  7282  oeeui  8587  resixp  8930  domssex  9125  cantnflem1a  9653  cantnflem1d  9656  cantnflem3  9659  cantnflem4  9660  fpwwe2lem6  10620  canthnumlem  10632  canthp1lem2  10637  wun0  10702  lelttrdi  11371  supmullem2  12185  supmul  12186  ixxdisj  13386  ixxun  13387  ixxss1  13389  ixxss2  13390  ixxss12  13391  ixxub  13392  ixxlb  13393  ubioo  13403  elicore  13424  iccgelb  13428  iccss2  13443  icodisj  13502  xov1plusxeqvd  13524  fldiv  13893  immul  15187  sqrtge0  15308  sqrtrege0  15417  icco1  15591  ruclem2  16287  ruclem3  16288  ruclem8  16292  ruclem12  16296  gcddvds  16560  crth  16836  phimullem  16837  eulerthlem1  16839  eulerthlem2  16840  prmreclem3  16977  sectcan  17811  sectco  17812  sectmon  17838  monsect  17839  funcixp  17923  funcsect  17928  invfuc  18033  coapm  18127  catciso  18167  posasymb  18374  ipodrsima  18596  pstr2  18626  psdmrn  18628  psref  18629  mhmlin  18850  subm0cl  18868  eqger  19245  eqgcpbl  19249  gaorber  19377  orbstafun  19380  cayleyth  19484  pmtrrn2  19529  pmtrfinv  19530  dfod2  19633  sylow2blem1  19689  dprdf  20077  dprdff  20083  dprdfcl  20084  dprdsplit  20119  dpjcntz  20123  ablfac1a  20140  ablfac1b  20141  lmodvsdi  20985  lbssp  21179  2idlcpblrng  21389  prmidlnr  21443  qsidomlem2  21460  evlsval3  22219  mpff  22242  mpfaddcl  22243  mpfmulcl  22244  mpfind  22245  pf1rcl  22488  mpfpf1  22490  mdetunilem2  22749  mdetunilem5  22752  mdetunilem6  22753  chfacfisfcpmat  22991  pnfnei  23356  cnptop2  23379  lmcl  23433  lmcnp  23440  flimfil  24105  tlmlmod  24325  ustbasel  24343  ustincl  24344  ustinvel  24346  ustfilxp  24349  tusunif  24404  imasdsf1olem  24509  xmeter  24569  tmsds  24620  metustexhalf  24692  nlmlmod  24814  qdensere  24905  blcvx  24934  tgqioo  24936  icccmplem2  24960  reconnlem1  24963  cnmpopc  25066  phtpcer  25133  phtpcco2  25137  pcohtpylem  25157  pcohtpy  25158  pcophtb  25167  om1addcl  25171  pi1blem  25177  pi1cpbl  25182  pi1grplem  25187  pi1inv  25190  pi1xfrf  25191  pi1xfr  25193  pi1xfrcnvlem  25194  pi1cof  25197  pi1coghm  25199  cphnlm  25310  cphsqrtcl2  25324  tcphcph  25375  lmcau  25451  bcthlem4  25465  minveclem4c  25563  minveclem2  25564  minveclem3b  25566  minveclem4  25570  minveclem6  25572  ivthicc  25596  ovolfsval  25608  ovollb2lem  25626  ovolshftlem1  25647  ovolscalem1  25651  ovolicc1  25654  ovolicc2lem2  25656  ovolicc2lem4  25658  ovolicc2lem5  25659  ovolicopnf  25662  ioombl1lem1  25696  ioombl1lem3  25698  ioombl1lem4  25699  uniioovol  25717  uniioombllem2a  25720  uniioombllem2  25721  uniioombllem3a  25722  uniioombllem3  25723  uniioombllem4  25724  uniioombllem6  25726  dyadmaxlem  25735  volivth  25745  vitalilem2  25747  vitalilem5  25750  i1frn  25815  itg2monolem1  25888  itgcnlem  25928  itgrevallem1  25933  itgreval  25935  itgle  25948  ibladd  25959  iblabslem  25966  itgspliticc  25975  itgsplitioo  25976  ditgcl  25996  ditgswap  25997  ditgsplitlem  25998  limcdif  26014  limcresi  26023  limccnp  26029  limccnp2  26030  limcco  26031  dvlip  26131  dvlip2  26133  dveq0  26138  dvgt0lem1  26140  dvivthlem1  26146  dvcnvrelem1  26155  dvcnvre  26157  dvfsumlem2  26165  ftc1lem1  26173  ftc1a  26175  ftc1lem4  26177  ftc2ditglem  26183  itgsubstlem  26186  ply1rem  26302  fta1glem1  26304  ig1pdvds  26316  plyrem  26445  facth  26446  fta1lem  26447  vieta1lem1  26450  vieta1lem2  26451  aaliou3lem3  26484  aaliou3lem4  26486  aaliou3lem7  26489  taylfvallem1  26496  tayl0  26501  taylply2  26507  radcnvle  26559  psercnlem2  26563  psercnlem1  26564  psercn  26565  pserdvlem1  26566  pserdvlem2  26567  abelth2  26581  coseq00topi  26643  coseq0negpitopi  26644  cosordlem  26671  tanord1  26678  efif1olem1  26683  loglesqrt  26902  logreclem  26903  relogbval  26913  nnlogbexp  26922  chordthmlem4  26976  quart1  26997  quartlem2  26999  quartlem3  27000  quartlem4  27001  quart  27002  acosbnd  27041  atancj  27051  atanlogsublem  27056  atantan  27064  atanbndlem  27066  dvatan  27076  atantayl  27078  rlimcnp2  27107  divsqrtsumlem  27120  ftalem5  27217  ftalem7  27219  basellem4  27224  basellem5  27225  perfectlem2  27370  dchrinv  27401  chpdifbndlem1  27693  pntibndlem2  27731  pntlemc  27735  pntlema  27736  pntlemb  27737  pntlemg  27738  pntlemh  27739  pntlemq  27741  pntlemr  27742  pntlemj  27743  pntlemi  27744  pntlemf  27745  pntlemk  27746  pntlemo  27747  pntleme  27748  pntlem3  27749  pntleml  27751  abvcxp  27755  cutsun12  27959  lesrec  27968  eqcuts3  27973  cofcut2  28091  cofcutr  28093  cofcutrtime  28096  cutmax  28103  cutmin  28104  addsproplem4  28141  addsproplem6  28143  addsuniflem  28170  addsasslem1  28172  addsasslem2  28173  negsproplem5  28201  negsproplem6  28202  negcut2  28209  negsunif  28224  mulsproplem12  28296  sltmuls1  28316  sltmuls2  28317  mulsuniflem  28318  precsexlem11  28386  twocut  28592  pw2cut2  28631  axtgpasch  28712  cgr3simp2  28766  legso  28844  hlne2  28854  hlln  28855  mirhl  28932  inagswap  29131  inagne2  29133  dfcgrg2  29153  subumgredg2  29601  upgrres1  29629  nb3grprlem1  29696  wlkp  29932  wspthsswwlkn  30233  2wlkdlem6  30246  clwwisshclwwsn  30333  erclwwlkeqlen  30336  erclwwlksym  30338  erclwwlktr  30339  clwwlkn  30343  clwwlknwrd  30351  clwwlknonex2e  30427  grpoass  30821  vcsm  30880  nvf  30978  ssps  31048  minvecolem2  31193  minvecolem4c  31197  minvecolem4  31198  minvecolem5  31199  minvecolem6  31200  eigvec1  32280  eliccelico  33088  elicoelioo  33089  pmtrto1cl  33385  cyc3evpm  33436  slmdvsdi  33501  slmdvs1  33506  sdrgdvcl  33586  sdrginvcl  33587  fldgenssp  33605  imaslmod  33639  mxidlnr  33713  0ringmon1p  33813  irngnzply1lem  34046  irngnzply1  34047  ply1annig1p  34060  minplycl  34062  ply1annprmidl  34063  minplym1p  34069  minplynzm1p  34070  algextdeglem1  34073  algextdeglem2  34074  algextdeglem3  34075  algextdeglem4  34076  algextdeglem5  34077  constrsqrtcl  34135  cnre2csqlem  34266  lmxrge0  34308  sigaclci  34488  difelsiga  34489  insiga  34493  ldsysgenld  34516  sigapildsyslem  34517  sigapildsys  34518  ldgenpisyslem1  34519  measvnul  34562  sibfrn  34693  eulerpartlemt  34727  eulerpartlemmf  34731  tg5segofs  35029  lpadleft  35039  spthcycl  35587  subgrwlk  35590  acycgrcycl  35605  subfacp1lem2a  35638  subfacp1lem3  35640  subfacp1lem4  35641  subfacp1lem5  35642  sconnpht2  35696  sconnpi1  35697  resconn  35704  cvmsss  35725  cvmsn0  35726  cvmlift2lem3  35763  cvmlift2lem7  35767  cvmliftphtlem  35775  cvmliftpht  35776  cvmlift3lem5  35781  cvmlift3lem6  35782  msrf  36000  elmsta  36006  mclsax  36027  mthmpps  36040  mclspps  36042  ivthALT  36812  weiunpo  36942  weiunso  36943  weiunfr  36944  weiunse  36945  poimirlem17  38254  poimirlem20  38257  ibladdnc  38294  iblabsnclem  38300  ftc1cnnclem  38308  ftc1anc  38318  ftc2nc  38319  heiborlem3  38430  iccbnd  38457  rngohom1  38585  idl0cl  38635  maxidlnr  38659  lshpne  39724  opococ  39937  opexmid  39949  hlclat  40100  lclkrslem2  42280  fzne2d  42715  dvrelog2  42799  dvrelog3  42800  0nonelalab  42802  aks4d1p1p5  42810  primrootsunit1  42832  primrootscoprmpow  42834  primrootscoprbij  42837  primrootspoweq0  42841  aks6d1c2lem3  42861  aks6d1c2  42865  aks6d1c6lem5  42912  aks5lem1  42921  aks5lem2  42922  aks5lem3a  42924  aks5lem5a  42926  unitscyglem1  42930  flt4lem5f  43359  flt4lem7  43361  nna4b4nsq  43362  gneispacern2  44835  cvgdvgrat  44993  iccshift  46204  iccsuble  46205  icoiccdif  46210  mullimc  46302  limccog  46306  mullimcf  46309  lptioo2  46317  limcmptdm  46319  limcicciooub  46321  xlimmnfvlem1  46516  xlimpnfvlem1  46520  icccncfext  46571  cncfioobdlem  46580  ditgeqiooicc  46644  itgsubsticc  46660  iblcncfioo  46662  itgiccshift  46664  itgperiod  46665  itgsbtaddcnst  46666  stoweidlem31  46715  stoweidlem36  46720  stoweidlem38  46722  stoweidlem44  46728  stoweidlem62  46746  dirkercncflem1  46787  dirkercncflem4  46790  fourierdlem26  46817  fourierdlem32  46823  fourierdlem33  46824  fourierdlem37  46828  fourierdlem42  46833  fourierdlem54  46844  fourierdlem63  46853  fourierdlem64  46854  fourierdlem65  46855  fourierdlem69  46859  fourierdlem74  46864  fourierdlem75  46865  fourierdlem79  46869  fourierdlem81  46871  fourierdlem82  46872  fourierdlem89  46879  fourierdlem90  46880  fourierdlem91  46881  fourierdlem93  46883  fourierdlem101  46891  fourierdlem111  46901  saldifcl  47003  unisalgen2  47038  hoidmv1lelem3  47277  smff  47416  sigardiv  47545  sigarcol  47548  sharhght  47549  sigaradd  47550  cevathlem1  47551  cevathlem2  47552  cevath  47553  proththd  48333  perfectALTVlem2  48454  gpgnbgrvtx0  48806  gpgnbgrvtx1  48807  imasubc2  49897  imaf1co  49900  idfullsubc  49906  fucofulem1  50055