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  7256  f1dom3el3dif  7257  f1prex  7272  oeeui  8608  resixp  8941  domssex  9146  cantnflem1a  9691  cantnflem1d  9694  cantnflem3  9697  cantnflem4  9698  fpwwe2lem6  10642  canthnumlem  10654  canthp1lem2  10659  wun0  10724  lelttrdi  11389  supmullem2  12205  supmul  12206  ixxdisj  13368  ixxun  13369  ixxss1  13371  ixxss2  13372  ixxss12  13373  ixxub  13374  ixxlb  13375  ubioo  13385  elicore  13405  iccgelb  13409  iccss2  13424  icodisj  13482  xov1plusxeqvd  13504  fldiv  13866  immul  15142  sqrtge0  15263  sqrtrege0  15371  icco1  15543  ruclem2  16235  ruclem3  16236  ruclem8  16240  ruclem12  16244  gcddvds  16507  crth  16782  phimullem  16783  eulerthlem1  16785  eulerthlem2  16786  prmreclem3  16923  sectcan  17753  sectco  17754  sectmon  17780  monsect  17781  funcixp  17865  funcsect  17870  invfuc  17975  coapm  18069  catciso  18109  posasymb  18316  ipodrsima  18536  pstr2  18566  psdmrn  18568  psref  18569  mhmlin  18756  subm0cl  18774  eqger  19146  eqgcpbl  19150  gaorber  19276  orbstafun  19279  cayleyth  19381  pmtrrn2  19426  pmtrfinv  19427  dfod2  19530  sylow2blem1  19586  dprdf  19974  dprdff  19980  dprdfcl  19981  dprdsplit  20016  dpjcntz  20020  ablfac1a  20037  ablfac1b  20038  lmodvsdi  20827  lbssp  21022  2idlcpblrng  21217  mpff  22047  mpfaddcl  22048  mpfmulcl  22049  mpfind  22050  pf1rcl  22272  mpfpf1  22274  mdetunilem2  22536  mdetunilem5  22539  mdetunilem6  22540  chfacfisfcpmat  22778  pnfnei  23143  cnptop2  23166  lmcl  23220  lmcnp  23227  flimfil  23892  tlmlmod  24112  ustbasel  24130  ustincl  24131  ustinvel  24133  ustfilxp  24136  tusunif  24192  imasdsf1olem  24297  xmeter  24357  tmsds  24408  metustexhalf  24480  nlmlmod  24602  qdensere  24693  blcvx  24722  tgqioo  24724  icccmplem2  24748  reconnlem1  24751  cnmpopc  24858  phtpcer  24930  phtpcco2  24935  pcohtpylem  24955  pcohtpy  24956  pcophtb  24965  om1addcl  24969  pi1blem  24975  pi1cpbl  24980  pi1grplem  24985  pi1inv  24988  pi1xfrf  24989  pi1xfr  24991  pi1xfrcnvlem  24992  pi1cof  24995  pi1coghm  24997  cphnlm  25109  cphsqrtcl2  25123  tcphcph  25174  lmcau  25250  bcthlem4  25264  minveclem4c  25362  minveclem2  25363  minveclem3b  25365  minveclem4  25369  minveclem6  25371  ivthicc  25396  ovolfsval  25408  ovollb2lem  25426  ovolshftlem1  25447  ovolscalem1  25451  ovolicc1  25454  ovolicc2lem2  25456  ovolicc2lem4  25458  ovolicc2lem5  25459  ovolicopnf  25462  ioombl1lem1  25496  ioombl1lem3  25498  ioombl1lem4  25499  uniioovol  25517  uniioombllem2a  25520  uniioombllem2  25521  uniioombllem3a  25522  uniioombllem3  25523  uniioombllem4  25524  uniioombllem6  25526  dyadmaxlem  25535  volivth  25545  vitalilem2  25547  vitalilem5  25550  i1frn  25615  itg2monolem1  25688  itgcnlem  25728  itgrevallem1  25733  itgreval  25735  itgle  25748  ibladd  25759  iblabslem  25766  itgspliticc  25775  itgsplitioo  25776  ditgcl  25796  ditgswap  25797  ditgsplitlem  25798  limcdif  25814  limcresi  25823  limccnp  25829  limccnp2  25830  limcco  25831  dvlip  25935  dvlip2  25937  dveq0  25942  dvgt0lem1  25944  dvivthlem1  25950  dvcnvrelem1  25959  dvcnvre  25961  dvfsumlem2  25970  dvfsumlem2OLD  25971  ftc1lem1  25979  ftc1a  25981  ftc1lem4  25983  ftc2ditglem  25989  itgsubstlem  25992  ply1rem  26108  fta1glem1  26110  ig1pdvds  26122  plyrem  26250  facth  26251  fta1lem  26252  vieta1lem1  26255  vieta1lem2  26256  aaliou3lem3  26289  aaliou3lem4  26291  aaliou3lem7  26294  taylfvallem1  26301  tayl0  26306  taylply2  26312  taylply2OLD  26313  radcnvle  26366  psercnlem2  26371  psercnlem1  26372  psercn  26373  pserdvlem1  26374  pserdvlem2  26375  abelth2  26389  coseq00topi  26447  coseq0negpitopi  26448  cosordlem  26475  tanord1  26482  efif1olem1  26487  loglesqrt  26707  logreclem  26708  relogbval  26718  nnlogbexp  26727  chordthmlem4  26781  quart1  26802  quartlem2  26804  quartlem3  26805  quartlem4  26806  quart  26807  acosbnd  26846  atancj  26856  atanlogsublem  26861  atantan  26869  atanbndlem  26871  dvatan  26881  atantayl  26883  rlimcnp2  26912  divsqrtsumlem  26926  ftalem5  27023  ftalem7  27025  basellem4  27030  basellem5  27031  perfectlem2  27177  dchrinv  27208  chpdifbndlem1  27500  pntibndlem2  27538  pntlemc  27542  pntlema  27543  pntlemb  27544  pntlemg  27545  pntlemh  27546  pntlemq  27548  pntlemr  27549  pntlemj  27550  pntlemi  27551  pntlemf  27552  pntlemk  27553  pntlemo  27554  pntleme  27555  pntlem3  27556  pntleml  27558  abvcxp  27562  scutun12  27758  slerec  27767  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  28056  ssltmul1  28076  ssltmul2  28077  mulsuniflem  28078  precsexlem11  28144  axtgpasch  28378  cgr3simp2  28432  legso  28510  hlne2  28517  hlln  28518  mirhl  28590  inagswap  28752  inagne2  28754  dfcgrg2  28774  subumgredg2  29196  upgrres1  29224  nb3grprlem1  29291  wlkp  29528  wspthsswwlkn  29832  2wlkdlem6  29845  clwwisshclwwsn  29929  erclwwlkeqlen  29932  erclwwlksym  29934  erclwwlktr  29935  clwwlkn  29939  clwwlknwrd  29947  clwwlknonex2e  30023  grpoass  30416  vcsm  30475  nvf  30573  ssps  30643  minvecolem2  30788  minvecolem4c  30792  minvecolem4  30793  minvecolem5  30794  minvecolem6  30795  eigvec1  31875  eliccelico  32688  elicoelioo  32689  pmtrto1cl  33028  cyc3evpm  33079  slmdvsdi  33130  slmdvs1  33135  sdrgdvcl  33211  sdrginvcl  33212  fldgenssp  33230  imaslmod  33286  prmidlnr  33372  qsidomlem2  33386  mxidlnr  33397  0ringmon1p  33488  irngnzply1lem  33647  irngnzply1  33648  ply1annig1p  33654  minplycl  33656  ply1annprmidl  33657  minplym1p  33663  minplynzm1p  33664  algextdeglem1  33667  algextdeglem2  33668  algextdeglem3  33669  algextdeglem4  33670  algextdeglem5  33671  constrsqrtcl  33729  cnre2csqlem  33849  lmxrge0  33891  sigaclci  34071  difelsiga  34072  insiga  34076  ldsysgenld  34099  sigapildsyslem  34100  sigapildsys  34101  ldgenpisyslem1  34102  measvnul  34145  sibfrn  34277  eulerpartlemt  34311  eulerpartlemmf  34315  tg5segofs  34626  lpadleft  34636  spthcycl  35072  subgrwlk  35075  acycgrcycl  35090  subfacp1lem2a  35123  subfacp1lem3  35125  subfacp1lem4  35126  subfacp1lem5  35127  sconnpht2  35181  sconnpi1  35182  resconn  35189  cvmsss  35210  cvmsn0  35211  cvmlift2lem3  35248  cvmlift2lem7  35252  cvmliftphtlem  35260  cvmliftpht  35261  cvmlift3lem5  35266  cvmlift3lem6  35267  msrf  35485  elmsta  35491  mclsax  35512  mthmpps  35525  mclspps  35527  ivthALT  36274  weiunpo  36404  weiunso  36405  weiunfr  36406  weiunse  36407  poimirlem17  37582  poimirlem20  37585  ibladdnc  37622  iblabsnclem  37628  ftc1cnnclem  37636  ftc1anc  37646  ftc2nc  37647  heiborlem3  37758  iccbnd  37785  rngohom1  37913  idl0cl  37963  maxidlnr  37987  lshpne  38921  opococ  39134  opexmid  39146  hlclat  39297  lclkrslem2  41478  fzne2d  41915  dvrelog2  41999  dvrelog3  42000  0nonelalab  42002  aks4d1p1p5  42010  primrootsunit1  42032  primrootscoprmpow  42034  primrootscoprbij  42037  primrootspoweq0  42041  aks6d1c2lem3  42061  aks6d1c2  42065  aks6d1c6lem5  42112  aks5lem1  42121  aks5lem2  42122  aks5lem3a  42124  aks5lem5a  42126  unitscyglem1  42130  metakunt8  42147  metakunt21  42160  metakunt22  42161  metakunt24  42163  metakunt25  42164  evlsval3  42507  flt4lem5f  42605  flt4lem7  42607  nna4b4nsq  42608  gneispacern2  44088  cvgdvgrat  44263  iccshift  45475  iccsuble  45476  icoiccdif  45481  mullimc  45575  limccog  45579  mullimcf  45582  lptioo2  45590  limcmptdm  45594  limcicciooub  45596  xlimmnfvlem1  45791  xlimpnfvlem1  45795  icccncfext  45846  cncfioobdlem  45855  ditgeqiooicc  45919  itgsubsticc  45935  iblcncfioo  45937  itgiccshift  45939  itgperiod  45940  itgsbtaddcnst  45941  stoweidlem31  45990  stoweidlem36  45995  stoweidlem38  45997  stoweidlem44  46003  stoweidlem62  46021  dirkercncflem1  46062  dirkercncflem4  46065  fourierdlem26  46092  fourierdlem32  46098  fourierdlem33  46099  fourierdlem37  46103  fourierdlem42  46108  fourierdlem54  46119  fourierdlem63  46128  fourierdlem64  46129  fourierdlem65  46130  fourierdlem69  46134  fourierdlem74  46139  fourierdlem75  46140  fourierdlem79  46144  fourierdlem81  46146  fourierdlem82  46147  fourierdlem89  46154  fourierdlem90  46155  fourierdlem91  46156  fourierdlem93  46158  fourierdlem101  46166  fourierdlem111  46176  saldifcl  46278  unisalgen2  46313  hoidmv1lelem3  46552  smff  46691  sigardiv  46820  sigarcol  46823  sharhght  46824  sigaradd  46825  cevathlem1  46826  cevathlem2  46827  cevath  46828  proththd  47546  perfectALTVlem2  47654  gpgnbgrvtx0  47975  gpgnbgrvtx1  47976  fucofulem1  49027