Theorem simp2d 1140

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

Syntax hints:   → wi 4   ∧ w3a 1084

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 400  df-3an 1086

This theorem is referenced by:  simp2bi  1143  f1dom3fv3dif  7004  f1dom3el3dif  7005  f1prex  7018  oeeui  8211  resixp  8480  domssex  8662  cantnflem1a  9132  cantnflem1d  9135  cantnflem3  9138  cantnflem4  9139  fpwwe2lem7  10047  canthnumlem  10059  canthp1lem2  10064  wun0  10129  lelttrdi  10791  supmullem2  11599  supmul  11600  ixxdisj  12741  ixxun  12742  ixxss1  12744  ixxss2  12745  ixxss12  12746  ixxub  12747  ixxlb  12748  ubioo  12758  elicore  12777  iccgelb  12781  iccss2  12796  icodisj  12854  xov1plusxeqvd  12876  fldiv  13223  immul  14487  sqrtge0  14609  sqrtrege0  14717  icco1  14889  ruclem2  15577  ruclem3  15578  ruclem8  15582  ruclem12  15586  gcddvds  15842  crth  16105  phimullem  16106  eulerthlem1  16108  eulerthlem2  16109  prmreclem3  16244  sectcan  17017  sectco  17018  sectmon  17044  monsect  17045  funcixp  17129  funcsect  17134  invfuc  17236  coapm  17323  catciso  17359  posasymb  17554  ipodrsima  17767  pstr2  17807  psdmrn  17809  psref  17810  mhmlin  17955  subm0cl  17968  eqger  18322  eqgcpbl  18326  gaorber  18430  orbstafun  18433  cayleyth  18535  pmtrrn2  18580  pmtrfinv  18581  dfod2  18683  sylow2blem1  18737  dprdf  19121  dprdff  19127  dprdfcl  19128  dprdsplit  19163  dpjcntz  19167  ablfac1a  19184  ablfac1b  19185  lmodvsdi  19650  lbssp  19844  2idlcpbl  20000  assaring  20550  mpff  20776  mpfaddcl  20777  mpfmulcl  20778  mpfind  20779  pf1rcl  20973  mpfpf1  20975  mdetunilem2  21218  mdetunilem5  21221  mdetunilem6  21222  chfacfisfcpmat  21460  pnfnei  21825  cnptop2  21848  lmcl  21902  lmcnp  21909  flimfil  22574  tlmlmod  22794  ustbasel  22812  ustincl  22813  ustinvel  22815  ustfilxp  22818  tusunif  22875  imasdsf1olem  22980  xmeter  23040  tmsds  23091  metustexhalf  23163  nlmlmod  23284  qdensere  23375  blcvx  23403  tgqioo  23405  icccmplem2  23428  reconnlem1  23431  cnmpopc  23533  phtpcer  23600  phtpcco2  23604  pcohtpylem  23624  pcohtpy  23625  pcophtb  23634  om1addcl  23638  pi1blem  23644  pi1cpbl  23649  pi1grplem  23654  pi1inv  23657  pi1xfrf  23658  pi1xfr  23660  pi1xfrcnvlem  23661  pi1cof  23664  pi1coghm  23666  cphnlm  23777  cphsqrtcl2  23791  tcphcph  23841  lmcau  23917  bcthlem4  23931  minveclem4c  24029  minveclem2  24030  minveclem3b  24032  minveclem4  24036  minveclem6  24038  ivthicc  24062  ovolfsval  24074  ovollb2lem  24092  ovolshftlem1  24113  ovolscalem1  24117  ovolicc1  24120  ovolicc2lem2  24122  ovolicc2lem4  24124  ovolicc2lem5  24125  ovolicopnf  24128  ioombl1lem1  24162  ioombl1lem3  24164  ioombl1lem4  24165  uniioovol  24183  uniioombllem2a  24186  uniioombllem2  24187  uniioombllem3a  24188  uniioombllem3  24189  uniioombllem4  24190  uniioombllem6  24192  dyadmaxlem  24201  volivth  24211  vitalilem2  24213  vitalilem5  24216  i1frn  24281  itg2monolem1  24354  itgcnlem  24393  itgrevallem1  24398  itgreval  24400  itgle  24413  ibladd  24424  iblabslem  24431  itgspliticc  24440  itgsplitioo  24441  ditgcl  24461  ditgswap  24462  ditgsplitlem  24463  limcdif  24479  limcresi  24488  limccnp  24494  limccnp2  24495  limcco  24496  dvlip  24596  dvlip2  24598  dveq0  24603  dvgt0lem1  24605  dvivthlem1  24611  dvcnvrelem1  24620  dvcnvre  24622  dvfsumlem2  24630  ftc1lem1  24638  ftc1a  24640  ftc1lem4  24642  ftc2ditglem  24648  itgsubstlem  24651  ply1rem  24764  fta1glem1  24766  ig1pdvds  24777  plyrem  24901  facth  24902  fta1lem  24903  vieta1lem1  24906  vieta1lem2  24907  aaliou3lem3  24940  aaliou3lem4  24942  aaliou3lem7  24945  taylfvallem1  24952  tayl0  24957  taylply2  24963  radcnvle  25015  psercnlem2  25019  psercnlem1  25020  psercn  25021  pserdvlem1  25022  pserdvlem2  25023  abelth2  25037  coseq00topi  25095  coseq0negpitopi  25096  cosordlem  25122  tanord1  25129  efif1olem1  25134  loglesqrt  25347  logreclem  25348  relogbval  25358  nnlogbexp  25367  chordthmlem4  25421  quart1  25442  quartlem2  25444  quartlem3  25445  quartlem4  25446  quart  25447  acosbnd  25486  atancj  25496  atanlogsublem  25501  atantan  25509  atanbndlem  25511  dvatan  25521  atantayl  25523  rlimcnp2  25552  divsqrtsumlem  25565  ftalem5  25662  ftalem7  25664  basellem4  25669  basellem5  25670  perfectlem2  25814  dchrinv  25845  chpdifbndlem1  26137  pntibndlem2  26175  pntlemc  26179  pntlema  26180  pntlemb  26181  pntlemg  26182  pntlemh  26183  pntlemq  26185  pntlemr  26186  pntlemj  26187  pntlemi  26188  pntlemf  26189  pntlemk  26190  pntlemo  26191  pntleme  26192  pntlem3  26193  pntleml  26195  abvcxp  26199  axtgpasch  26261  cgr3simp2  26315  legso  26393  hlne2  26400  hlln  26401  mirhl  26473  inagswap  26635  inagne2  26637  dfcgrg2  26657  subumgredg2  27075  upgrres1  27103  nb3grprlem1  27170  wlkp  27406  wspthsswwlkn  27704  2wlkdlem6  27717  clwwisshclwwsn  27801  erclwwlkeqlen  27804  erclwwlksym  27806  erclwwlktr  27807  clwwlkn  27811  clwwlknwrd  27819  clwwlknonex2e  27895  grpoass  28286  vcsm  28345  nvf  28443  ssps  28513  minvecolem2  28658  minvecolem4c  28662  minvecolem4  28663  minvecolem5  28664  minvecolem6  28665  eigvec1  29745  eliccelico  30526  elicoelioo  30527  pmtrto1cl  30791  cyc3evpm  30842  slmdvsdi  30893  slmdvs1  30898  imaslmod  30973  prmidlnr  31022  qsidomlem2  31037  mxidlnr  31044  cnre2csqlem  31263  lmxrge0  31305  sigaclci  31501  difelsiga  31502  insiga  31506  ldsysgenld  31529  sigapildsyslem  31530  sigapildsys  31531  ldgenpisyslem1  31532  measvnul  31575  sibfrn  31705  eulerpartlemt  31739  eulerpartlemmf  31743  tg5segofs  32054  lpadleft  32064  spthcycl  32489  subgrwlk  32492  acycgrcycl  32507  subfacp1lem2a  32540  subfacp1lem3  32542  subfacp1lem4  32543  subfacp1lem5  32544  sconnpht2  32598  sconnpi1  32599  resconn  32606  cvmsss  32627  cvmsn0  32628  cvmlift2lem3  32665  cvmlift2lem7  32669  cvmliftphtlem  32677  cvmliftpht  32678  cvmlift3lem5  32683  cvmlift3lem6  32684  msrf  32902  elmsta  32908  mclsax  32929  mthmpps  32942  mclspps  32944  scutun12  33384  slerec  33390  ivthALT  33796  poimirlem17  35074  poimirlem20  35077  ibladdnc  35114  iblabsnclem  35120  ftc1cnnclem  35128  ftc1anc  35138  ftc2nc  35139  heiborlem3  35251  iccbnd  35278  rngohom1  35406  idl0cl  35456  maxidlnr  35480  lshpne  36278  opococ  36491  opexmid  36503  hlclat  36654  lclkrslem2  38834  fzne2d  39268  metakunt8  39357  metakunt21  39370  metakunt22  39371  metakunt24  39373  metakunt25  39374  gneispacern2  40842  cvgdvgrat  41017  iccshift  42155  iccsuble  42156  icoiccdif  42161  mullimc  42258  limccog  42262  mullimcf  42265  lptioo2  42273  limcmptdm  42277  limcicciooub  42279  xlimmnfvlem1  42474  xlimpnfvlem1  42478  icccncfext  42529  cncfioobdlem  42538  ditgeqiooicc  42602  itgsubsticc  42618  iblcncfioo  42620  itgiccshift  42622  itgperiod  42623  itgsbtaddcnst  42624  stoweidlem11  42653  stoweidlem31  42673  stoweidlem36  42678  stoweidlem38  42680  stoweidlem44  42686  stoweidlem62  42704  dirkercncflem1  42745  dirkercncflem4  42748  fourierdlem26  42775  fourierdlem32  42781  fourierdlem33  42782  fourierdlem37  42786  fourierdlem42  42791  fourierdlem54  42802  fourierdlem63  42811  fourierdlem64  42812  fourierdlem65  42813  fourierdlem69  42817  fourierdlem74  42822  fourierdlem75  42823  fourierdlem79  42827  fourierdlem81  42829  fourierdlem82  42830  fourierdlem89  42837  fourierdlem90  42838  fourierdlem91  42839  fourierdlem93  42841  fourierdlem101  42849  fourierdlem111  42859  saldifcl  42961  unisalgen2  42994  hoidmv1lelem3  43232  smff  43366  smfpimltxr  43381  sigardiv  43475  sigarcol  43478  sharhght  43479  sigaradd  43480  cevathlem1  43481  cevathlem2  43482  cevath  43483  proththd  44132  perfectALTVlem2  44240