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 1088

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 206  df-an 398  df-3an 1090

This theorem is referenced by:  simp2bi  1147  f1dom3fv3dif  7267  f1dom3el3dif  7268  f1prex  7282  oeeui  8602  resixp  8927  domssex  9138  cantnflem1a  9680  cantnflem1d  9683  cantnflem3  9686  cantnflem4  9687  fpwwe2lem6  10631  canthnumlem  10643  canthp1lem2  10648  wun0  10713  lelttrdi  11376  supmullem2  12185  supmul  12186  ixxdisj  13339  ixxun  13340  ixxss1  13342  ixxss2  13343  ixxss12  13344  ixxub  13345  ixxlb  13346  ubioo  13356  elicore  13376  iccgelb  13380  iccss2  13395  icodisj  13453  xov1plusxeqvd  13475  fldiv  13825  immul  15083  sqrtge0  15204  sqrtrege0  15312  icco1  15484  ruclem2  16175  ruclem3  16176  ruclem8  16180  ruclem12  16184  gcddvds  16444  crth  16711  phimullem  16712  eulerthlem1  16714  eulerthlem2  16715  prmreclem3  16851  sectcan  17702  sectco  17703  sectmon  17729  monsect  17730  funcixp  17817  funcsect  17822  invfuc  17927  coapm  18021  catciso  18061  posasymb  18272  ipodrsima  18494  pstr2  18524  psdmrn  18526  psref  18527  mhmlin  18679  subm0cl  18692  eqger  19058  eqgcpbl  19062  gaorber  19172  orbstafun  19175  cayleyth  19283  pmtrrn2  19328  pmtrfinv  19329  dfod2  19432  sylow2blem1  19488  dprdf  19876  dprdff  19882  dprdfcl  19883  dprdsplit  19918  dpjcntz  19922  ablfac1a  19939  ablfac1b  19940  lmodvsdi  20495  lbssp  20690  2idlcpbl  20871  mpff  21667  mpfaddcl  21668  mpfmulcl  21669  mpfind  21670  pf1rcl  21868  mpfpf1  21870  mdetunilem2  22115  mdetunilem5  22118  mdetunilem6  22119  chfacfisfcpmat  22357  pnfnei  22724  cnptop2  22747  lmcl  22801  lmcnp  22808  flimfil  23473  tlmlmod  23693  ustbasel  23711  ustincl  23712  ustinvel  23714  ustfilxp  23717  tusunif  23774  imasdsf1olem  23879  xmeter  23939  tmsds  23993  metustexhalf  24065  nlmlmod  24195  qdensere  24286  blcvx  24314  tgqioo  24316  icccmplem2  24339  reconnlem1  24342  cnmpopc  24444  phtpcer  24511  phtpcco2  24515  pcohtpylem  24535  pcohtpy  24536  pcophtb  24545  om1addcl  24549  pi1blem  24555  pi1cpbl  24560  pi1grplem  24565  pi1inv  24568  pi1xfrf  24569  pi1xfr  24571  pi1xfrcnvlem  24572  pi1cof  24575  pi1coghm  24577  cphnlm  24689  cphsqrtcl2  24703  tcphcph  24754  lmcau  24830  bcthlem4  24844  minveclem4c  24942  minveclem2  24943  minveclem3b  24945  minveclem4  24949  minveclem6  24951  ivthicc  24975  ovolfsval  24987  ovollb2lem  25005  ovolshftlem1  25026  ovolscalem1  25030  ovolicc1  25033  ovolicc2lem2  25035  ovolicc2lem4  25037  ovolicc2lem5  25038  ovolicopnf  25041  ioombl1lem1  25075  ioombl1lem3  25077  ioombl1lem4  25078  uniioovol  25096  uniioombllem2a  25099  uniioombllem2  25100  uniioombllem3a  25101  uniioombllem3  25102  uniioombllem4  25103  uniioombllem6  25105  dyadmaxlem  25114  volivth  25124  vitalilem2  25126  vitalilem5  25129  i1frn  25194  itg2monolem1  25268  itgcnlem  25307  itgrevallem1  25312  itgreval  25314  itgle  25327  ibladd  25338  iblabslem  25345  itgspliticc  25354  itgsplitioo  25355  ditgcl  25375  ditgswap  25376  ditgsplitlem  25377  limcdif  25393  limcresi  25402  limccnp  25408  limccnp2  25409  limcco  25410  dvlip  25510  dvlip2  25512  dveq0  25517  dvgt0lem1  25519  dvivthlem1  25525  dvcnvrelem1  25534  dvcnvre  25536  dvfsumlem2  25544  ftc1lem1  25552  ftc1a  25554  ftc1lem4  25556  ftc2ditglem  25562  itgsubstlem  25565  ply1rem  25681  fta1glem1  25683  ig1pdvds  25694  plyrem  25818  facth  25819  fta1lem  25820  vieta1lem1  25823  vieta1lem2  25824  aaliou3lem3  25857  aaliou3lem4  25859  aaliou3lem7  25862  taylfvallem1  25869  tayl0  25874  taylply2  25880  radcnvle  25932  psercnlem2  25936  psercnlem1  25937  psercn  25938  pserdvlem1  25939  pserdvlem2  25940  abelth2  25954  coseq00topi  26012  coseq0negpitopi  26013  cosordlem  26039  tanord1  26046  efif1olem1  26051  loglesqrt  26266  logreclem  26267  relogbval  26277  nnlogbexp  26286  chordthmlem4  26340  quart1  26361  quartlem2  26363  quartlem3  26364  quartlem4  26365  quart  26366  acosbnd  26405  atancj  26415  atanlogsublem  26420  atantan  26428  atanbndlem  26430  dvatan  26440  atantayl  26442  rlimcnp2  26471  divsqrtsumlem  26484  ftalem5  26581  ftalem7  26583  basellem4  26588  basellem5  26589  perfectlem2  26733  dchrinv  26764  chpdifbndlem1  27056  pntibndlem2  27094  pntlemc  27098  pntlema  27099  pntlemb  27100  pntlemg  27101  pntlemh  27102  pntlemq  27104  pntlemr  27105  pntlemj  27106  pntlemi  27107  pntlemf  27108  pntlemk  27109  pntlemo  27110  pntleme  27111  pntlem3  27112  pntleml  27114  abvcxp  27118  scutun12  27312  slerec  27321  cofcut2  27411  cofcutr  27413  cofcutrtime  27416  addsproplem4  27458  addsproplem6  27460  addsuniflem  27487  addsasslem1  27489  addsasslem2  27490  negsproplem5  27509  negsproplem6  27510  negscut2  27517  negsunif  27532  mulsproplem12  27586  ssltmul1  27605  ssltmul2  27606  mulsuniflem  27607  precsexlem11  27666  axtgpasch  27749  cgr3simp2  27803  legso  27881  hlne2  27888  hlln  27889  mirhl  27961  inagswap  28123  inagne2  28125  dfcgrg2  28145  subumgredg2  28573  upgrres1  28601  nb3grprlem1  28668  wlkp  28904  wspthsswwlkn  29203  2wlkdlem6  29216  clwwisshclwwsn  29300  erclwwlkeqlen  29303  erclwwlksym  29305  erclwwlktr  29306  clwwlkn  29310  clwwlknwrd  29318  clwwlknonex2e  29394  grpoass  29787  vcsm  29846  nvf  29944  ssps  30014  minvecolem2  30159  minvecolem4c  30163  minvecolem4  30164  minvecolem5  30165  minvecolem6  30166  eigvec1  31246  eliccelico  32019  elicoelioo  32020  pmtrto1cl  32289  cyc3evpm  32340  slmdvsdi  32391  slmdvs1  32396  sdrgdvcl  32428  sdrginvcl  32429  fldgenssp  32439  imaslmod  32499  prmidlnr  32588  qsidomlem2  32603  mxidlnr  32611  0ringmon1p  32667  irngnzply1lem  32785  irngnzply1  32786  ply1annig1p  32796  minplycl  32798  ply1annprmidl  32799  algextdeglem1  32803  cnre2csqlem  32921  lmxrge0  32963  sigaclci  33161  difelsiga  33162  insiga  33166  ldsysgenld  33189  sigapildsyslem  33190  sigapildsys  33191  ldgenpisyslem1  33192  measvnul  33235  sibfrn  33367  eulerpartlemt  33401  eulerpartlemmf  33405  tg5segofs  33716  lpadleft  33726  spthcycl  34151  subgrwlk  34154  acycgrcycl  34169  subfacp1lem2a  34202  subfacp1lem3  34204  subfacp1lem4  34205  subfacp1lem5  34206  sconnpht2  34260  sconnpi1  34261  resconn  34268  cvmsss  34289  cvmsn0  34290  cvmlift2lem3  34327  cvmlift2lem7  34331  cvmliftphtlem  34339  cvmliftpht  34340  cvmlift3lem5  34345  cvmlift3lem6  34346  msrf  34564  elmsta  34570  mclsax  34591  mthmpps  34604  mclspps  34606  gg-dvfsumlem2  35214  ivthALT  35268  poimirlem17  36553  poimirlem20  36556  ibladdnc  36593  iblabsnclem  36599  ftc1cnnclem  36607  ftc1anc  36617  ftc2nc  36618  heiborlem3  36729  iccbnd  36756  rngohom1  36884  idl0cl  36934  maxidlnr  36958  lshpne  37900  opococ  38113  opexmid  38125  hlclat  38276  lclkrslem2  40457  fzne2d  40894  dvrelog2  40977  dvrelog3  40978  0nonelalab  40980  aks4d1p1p5  40988  metakunt8  41040  metakunt21  41053  metakunt22  41054  metakunt24  41056  metakunt25  41057  evlsval3  41179  flt4lem5f  41447  flt4lem7  41449  nna4b4nsq  41450  gneispacern2  42938  cvgdvgrat  43120  iccshift  44279  iccsuble  44280  icoiccdif  44285  mullimc  44380  limccog  44384  mullimcf  44387  lptioo2  44395  limcmptdm  44399  limcicciooub  44401  xlimmnfvlem1  44596  xlimpnfvlem1  44600  icccncfext  44651  cncfioobdlem  44660  ditgeqiooicc  44724  itgsubsticc  44740  iblcncfioo  44742  itgiccshift  44744  itgperiod  44745  itgsbtaddcnst  44746  stoweidlem31  44795  stoweidlem36  44800  stoweidlem38  44802  stoweidlem44  44808  stoweidlem62  44826  dirkercncflem1  44867  dirkercncflem4  44870  fourierdlem26  44897  fourierdlem32  44903  fourierdlem33  44904  fourierdlem37  44908  fourierdlem42  44913  fourierdlem54  44924  fourierdlem63  44933  fourierdlem64  44934  fourierdlem65  44935  fourierdlem69  44939  fourierdlem74  44944  fourierdlem75  44945  fourierdlem79  44949  fourierdlem81  44951  fourierdlem82  44952  fourierdlem89  44959  fourierdlem90  44960  fourierdlem91  44961  fourierdlem93  44963  fourierdlem101  44971  fourierdlem111  44981  saldifcl  45083  unisalgen2  45118  hoidmv1lelem3  45357  smff  45496  sigardiv  45625  sigarcol  45628  sharhght  45629  sigaradd  45630  cevathlem1  45631  cevathlem2  45632  cevath  45633  proththd  46330  perfectALTVlem2  46438  2idlcpblrng  46814