Theorem simplbda 505

Description: Deduction eliminating a conjunct. (Contributed by NM, 22-Oct-2007.)

Hypothesis

Ref	Expression
simplbda.1	⊢ (𝜑 → (𝜓 ↔ (𝜒 ∧ 𝜃)))

Assertion

Ref	Expression
simplbda	⊢ ((𝜑 ∧ 𝜓) → 𝜃)

Proof of Theorem simplbda

Step	Hyp	Ref	Expression
1		simplbda.1	. . 3 ⊢ (𝜑 → (𝜓 ↔ (𝜒 ∧ 𝜃)))
2	1	biimpa 482	. 2 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 ∧ 𝜃))
3	2	simprd 501	1 ⊢ ((𝜑 ∧ 𝜓) → 𝜃)

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  cantnflem3  9719  fseqenlem2  10131  axdc3lem2  10556  fpwwe2lem11  10753  rlimsqzlem  15845  ramub1lem2  17234  invfun  17968  pltne  18535  cntzi  19573  odmulg  19800  subgslw  19860  frgpnabllem1  20117  cyggeninv  20127  ablfaclem3  20333  lsslmod  21265  rhmpreimaidl  21601  rhmpreimaprmidl  21665  psgnevpm  21925  pjff  22048  pjf2  22050  pjcss  22052  ocvpj  22053  evlslem3  22419  mhpdeg  22496  scmatscmid  22851  fvmptnn04ifc  23200  fvmptnn04ifd  23201  tgcl  23317  cldopn  23379  cncnp  23628  1stcelcls  23810  lly1stc  23845  refssex  23860  qtoptop2  24048  qtopid  24054  trfg  24240  flfneii  24341  fclsbas  24370  isfcf  24383  restutop  24586  restutopopn  24587  isucn2  24627  cfiluexsm  24638  cfilufg  24641  blgt0  24748  xblss2ps  24750  xblss2  24751  mopni  24841  metrest  24873  metustbl  24915  restmetu  24919  cfilss  25621  caun0  25632  cmetcaulem  25639  cfilresi  25646  cmetcusp  25705  cnlimci  26239  dvcl  26249  dvcnp  26269  dvcnp2  26270  dvnadd  26279  dvfsumrlimge0  26380  dvfsumrlim  26381  dvfsumrlim2  26382  fta1g  26518  plyeq0lem  26559  vieta1lem1  26663  vieta1lem2  26664  fsumharmonic  27369  dvdsflf1o  27544  dvdsflsumcom  27545  fsumvma  27570  vmadivsumb  27840  dchrisum0lem1a  27843  dchrisumlema  27845  dchrisumlem3  27848  dchrmusum2  27851  dchrvmasumlem2  27855  dchrvmasumiflem1  27858  dchrisum0fno1  27868  dchrisum0lem1b  27872  mulog2sumlem2  27892  vmalogdivsum2  27895  2vmadivsumlem  27897  selberglem2  27903  selbergb  27906  selberg2b  27909  selberg3lem1  27914  selberg4lem1  27917  pntpbnd1  27943  pntibndlem3  27949  pntlem3  27966  sltsleft  28276  sltsright  28277  cofcutr  28340  oppnid  29252  prlnghpg  29454  sspba  31359  sspg  31360  ssps  31362  sspn  31368  nmblore  31418  phpar  31456  ocorth  31923  elnlfn2  32561  foresf1o  33172  fnpreimac  33336  fpwrelmap  33395  elrgspnsubrunlem2  33879  kerunit  33956  0nellinds  33996  linds2eq  34006  dvdsruasso  34010  unitpidl1  34044  mxidlirredi  34066  dflringlem2  34097  rprmdvds  34121  rprmnz  34122  1arithufdlem3  34148  ply1unit  34177  ply1degltlss  34198  selvply1rhmlema  34220  selvply1rhmlem1  34222  esplyfvaln  34276  exsslsb  34299  ply1degltdimlem  34324  lindsunlem  34326  dimkerim  34329  irngss  34389  0ringirng  34391  irngnminplynz  34414  algextdeglem8  34426  reff  34541  cnre2csqlem  34612  fmcncfil  34633  elzrhunit  34679  qqhval2lem  34683  baselsiga  34817  signsply0  35250  k3n0k2lt  36024  cvmliftmolem1  36213  mclsppslem  36515  mclspps  36516  fnetr  37317  relowlssretop  38478  mbfresfi  38776  itg2addnclem  38781  itg2addnclem2  38782  sstotbnd2  38900  rngoiso1o  39105  pridl  39163  lfli  40310  lkrf0  40342  cvrne  40530  atcvr0  40537  psubspi  40996  psubcli2N  41188  lhp1cvr  41248  lautle  41333  diadmleN  42287  sn-eluzp1l  43558  prjspnnorm  43854  cvgdvgrat  45489  radcnvrat  45490  projf1o  46416  islptre  46836  islpcn  46854  icccncfext  47102  fdivmptf  49858  refdivmptf  49859  rege1logbrege0  49875  nelsubc2  50388  termcterm2  50854