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 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  1146  f1dom3fv3dif  7305  f1dom3el3dif  7306  f1prex  7320  oeeui  8658  resixp  8991  domssex  9204  cantnflem1a  9754  cantnflem1d  9757  cantnflem3  9760  cantnflem4  9761  fpwwe2lem6  10705  canthnumlem  10717  canthp1lem2  10722  wun0  10787  lelttrdi  11452  supmullem2  12266  supmul  12267  ixxdisj  13422  ixxun  13423  ixxss1  13425  ixxss2  13426  ixxss12  13427  ixxub  13428  ixxlb  13429  ubioo  13439  elicore  13459  iccgelb  13463  iccss2  13478  icodisj  13536  xov1plusxeqvd  13558  fldiv  13911  immul  15185  sqrtge0  15306  sqrtrege0  15414  icco1  15586  ruclem2  16280  ruclem3  16281  ruclem8  16285  ruclem12  16289  gcddvds  16549  crth  16825  phimullem  16826  eulerthlem1  16828  eulerthlem2  16829  prmreclem3  16965  sectcan  17816  sectco  17817  sectmon  17843  monsect  17844  funcixp  17931  funcsect  17936  invfuc  18044  coapm  18138  catciso  18178  posasymb  18389  ipodrsima  18611  pstr2  18641  psdmrn  18643  psref  18644  mhmlin  18828  subm0cl  18846  eqger  19218  eqgcpbl  19222  gaorber  19348  orbstafun  19351  cayleyth  19457  pmtrrn2  19502  pmtrfinv  19503  dfod2  19606  sylow2blem1  19662  dprdf  20050  dprdff  20056  dprdfcl  20057  dprdsplit  20092  dpjcntz  20096  ablfac1a  20113  ablfac1b  20114  lmodvsdi  20905  lbssp  21101  2idlcpblrng  21304  mpff  22151  mpfaddcl  22152  mpfmulcl  22153  mpfind  22154  pf1rcl  22374  mpfpf1  22376  mdetunilem2  22640  mdetunilem5  22643  mdetunilem6  22644  chfacfisfcpmat  22882  pnfnei  23249  cnptop2  23272  lmcl  23326  lmcnp  23333  flimfil  23998  tlmlmod  24218  ustbasel  24236  ustincl  24237  ustinvel  24239  ustfilxp  24242  tusunif  24299  imasdsf1olem  24404  xmeter  24464  tmsds  24518  metustexhalf  24590  nlmlmod  24720  qdensere  24811  blcvx  24839  tgqioo  24841  icccmplem2  24864  reconnlem1  24867  cnmpopc  24974  phtpcer  25046  phtpcco2  25051  pcohtpylem  25071  pcohtpy  25072  pcophtb  25081  om1addcl  25085  pi1blem  25091  pi1cpbl  25096  pi1grplem  25101  pi1inv  25104  pi1xfrf  25105  pi1xfr  25107  pi1xfrcnvlem  25108  pi1cof  25111  pi1coghm  25113  cphnlm  25225  cphsqrtcl2  25239  tcphcph  25290  lmcau  25366  bcthlem4  25380  minveclem4c  25478  minveclem2  25479  minveclem3b  25481  minveclem4  25485  minveclem6  25487  ivthicc  25512  ovolfsval  25524  ovollb2lem  25542  ovolshftlem1  25563  ovolscalem1  25567  ovolicc1  25570  ovolicc2lem2  25572  ovolicc2lem4  25574  ovolicc2lem5  25575  ovolicopnf  25578  ioombl1lem1  25612  ioombl1lem3  25614  ioombl1lem4  25615  uniioovol  25633  uniioombllem2a  25636  uniioombllem2  25637  uniioombllem3a  25638  uniioombllem3  25639  uniioombllem4  25640  uniioombllem6  25642  dyadmaxlem  25651  volivth  25661  vitalilem2  25663  vitalilem5  25666  i1frn  25731  itg2monolem1  25805  itgcnlem  25845  itgrevallem1  25850  itgreval  25852  itgle  25865  ibladd  25876  iblabslem  25883  itgspliticc  25892  itgsplitioo  25893  ditgcl  25913  ditgswap  25914  ditgsplitlem  25915  limcdif  25931  limcresi  25940  limccnp  25946  limccnp2  25947  limcco  25948  dvlip  26052  dvlip2  26054  dveq0  26059  dvgt0lem1  26061  dvivthlem1  26067  dvcnvrelem1  26076  dvcnvre  26078  dvfsumlem2  26087  dvfsumlem2OLD  26088  ftc1lem1  26096  ftc1a  26098  ftc1lem4  26100  ftc2ditglem  26106  itgsubstlem  26109  ply1rem  26225  fta1glem1  26227  ig1pdvds  26239  plyrem  26365  facth  26366  fta1lem  26367  vieta1lem1  26370  vieta1lem2  26371  aaliou3lem3  26404  aaliou3lem4  26406  aaliou3lem7  26409  taylfvallem1  26416  tayl0  26421  taylply2  26427  taylply2OLD  26428  radcnvle  26481  psercnlem2  26486  psercnlem1  26487  psercn  26488  pserdvlem1  26489  pserdvlem2  26490  abelth2  26504  coseq00topi  26562  coseq0negpitopi  26563  cosordlem  26590  tanord1  26597  efif1olem1  26602  loglesqrt  26822  logreclem  26823  relogbval  26833  nnlogbexp  26842  chordthmlem4  26896  quart1  26917  quartlem2  26919  quartlem3  26920  quartlem4  26921  quart  26922  acosbnd  26961  atancj  26971  atanlogsublem  26976  atantan  26984  atanbndlem  26986  dvatan  26996  atantayl  26998  rlimcnp2  27027  divsqrtsumlem  27041  ftalem5  27138  ftalem7  27140  basellem4  27145  basellem5  27146  perfectlem2  27292  dchrinv  27323  chpdifbndlem1  27615  pntibndlem2  27653  pntlemc  27657  pntlema  27658  pntlemb  27659  pntlemg  27660  pntlemh  27661  pntlemq  27663  pntlemr  27664  pntlemj  27665  pntlemi  27666  pntlemf  27667  pntlemk  27668  pntlemo  27669  pntleme  27670  pntlem3  27671  pntleml  27673  abvcxp  27677  scutun12  27873  slerec  27882  cofcut2  27974  cofcutr  27976  cofcutrtime  27979  cutmax  27986  cutmin  27987  addsproplem4  28023  addsproplem6  28025  addsuniflem  28052  addsasslem1  28054  addsasslem2  28055  negsproplem5  28082  negsproplem6  28083  negscut2  28090  negsunif  28105  mulsproplem12  28171  ssltmul1  28191  ssltmul2  28192  mulsuniflem  28193  precsexlem11  28259  axtgpasch  28493  cgr3simp2  28547  legso  28625  hlne2  28632  hlln  28633  mirhl  28705  inagswap  28867  inagne2  28869  dfcgrg2  28889  subumgredg2  29320  upgrres1  29348  nb3grprlem1  29415  wlkp  29652  wspthsswwlkn  29951  2wlkdlem6  29964  clwwisshclwwsn  30048  erclwwlkeqlen  30051  erclwwlksym  30053  erclwwlktr  30054  clwwlkn  30058  clwwlknwrd  30066  clwwlknonex2e  30142  grpoass  30535  vcsm  30594  nvf  30692  ssps  30762  minvecolem2  30907  minvecolem4c  30911  minvecolem4  30912  minvecolem5  30913  minvecolem6  30914  eigvec1  31994  eliccelico  32782  elicoelioo  32783  pmtrto1cl  33092  cyc3evpm  33143  slmdvsdi  33194  slmdvs1  33199  sdrgdvcl  33266  sdrginvcl  33267  fldgenssp  33285  imaslmod  33346  prmidlnr  33432  qsidomlem2  33446  mxidlnr  33457  0ringmon1p  33548  irngnzply1lem  33690  irngnzply1  33691  ply1annig1p  33697  minplycl  33699  ply1annprmidl  33700  minplym1p  33706  algextdeglem1  33708  algextdeglem2  33709  algextdeglem3  33710  algextdeglem4  33711  algextdeglem5  33712  cnre2csqlem  33856  lmxrge0  33898  sigaclci  34096  difelsiga  34097  insiga  34101  ldsysgenld  34124  sigapildsyslem  34125  sigapildsys  34126  ldgenpisyslem1  34127  measvnul  34170  sibfrn  34302  eulerpartlemt  34336  eulerpartlemmf  34340  tg5segofs  34650  lpadleft  34660  spthcycl  35097  subgrwlk  35100  acycgrcycl  35115  subfacp1lem2a  35148  subfacp1lem3  35150  subfacp1lem4  35151  subfacp1lem5  35152  sconnpht2  35206  sconnpi1  35207  resconn  35214  cvmsss  35235  cvmsn0  35236  cvmlift2lem3  35273  cvmlift2lem7  35277  cvmliftphtlem  35285  cvmliftpht  35286  cvmlift3lem5  35291  cvmlift3lem6  35292  msrf  35510  elmsta  35516  mclsax  35537  mthmpps  35550  mclspps  35552  ivthALT  36301  weiunpo  36431  weiunso  36432  weiunfr  36433  weiunse  36434  poimirlem17  37597  poimirlem20  37600  ibladdnc  37637  iblabsnclem  37643  ftc1cnnclem  37651  ftc1anc  37661  ftc2nc  37662  heiborlem3  37773  iccbnd  37800  rngohom1  37928  idl0cl  37978  maxidlnr  38002  lshpne  38938  opococ  39151  opexmid  39163  hlclat  39314  lclkrslem2  41495  fzne2d  41937  dvrelog2  42021  dvrelog3  42022  0nonelalab  42024  aks4d1p1p5  42032  primrootsunit1  42054  primrootscoprmpow  42056  primrootscoprbij  42059  primrootspoweq0  42063  aks6d1c2lem3  42083  aks6d1c2  42087  aks6d1c6lem5  42134  aks5lem1  42143  aks5lem2  42144  aks5lem3a  42146  aks5lem5a  42148  unitscyglem1  42152  metakunt8  42169  metakunt21  42182  metakunt22  42183  metakunt24  42185  metakunt25  42186  evlsval3  42514  flt4lem5f  42612  flt4lem7  42614  nna4b4nsq  42615  gneispacern2  44101  cvgdvgrat  44282  iccshift  45436  iccsuble  45437  icoiccdif  45442  mullimc  45537  limccog  45541  mullimcf  45544  lptioo2  45552  limcmptdm  45556  limcicciooub  45558  xlimmnfvlem1  45753  xlimpnfvlem1  45757  icccncfext  45808  cncfioobdlem  45817  ditgeqiooicc  45881  itgsubsticc  45897  iblcncfioo  45899  itgiccshift  45901  itgperiod  45902  itgsbtaddcnst  45903  stoweidlem31  45952  stoweidlem36  45957  stoweidlem38  45959  stoweidlem44  45965  stoweidlem62  45983  dirkercncflem1  46024  dirkercncflem4  46027  fourierdlem26  46054  fourierdlem32  46060  fourierdlem33  46061  fourierdlem37  46065  fourierdlem42  46070  fourierdlem54  46081  fourierdlem63  46090  fourierdlem64  46091  fourierdlem65  46092  fourierdlem69  46096  fourierdlem74  46101  fourierdlem75  46102  fourierdlem79  46106  fourierdlem81  46108  fourierdlem82  46109  fourierdlem89  46116  fourierdlem90  46117  fourierdlem91  46118  fourierdlem93  46120  fourierdlem101  46128  fourierdlem111  46138  saldifcl  46240  unisalgen2  46275  hoidmv1lelem3  46514  smff  46653  sigardiv  46782  sigarcol  46785  sharhght  46786  sigaradd  46787  cevathlem1  46788  cevathlem2  46789  cevath  46790  proththd  47488  perfectALTVlem2  47596