Theorem simplbda 500

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 477	. 2 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 ∧ 𝜃))
3	2	simprd 496	1 ⊢ ((𝜑 ∧ 𝜓) → 𝜃)

Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  cantnflem3  9610  fseqenlem2  9945  axdc3lem2  10371  fpwwe2lem11  10562  rlimsqzlem  15609  ramub1lem2  16996  invfun  17729  pltne  18296  cntzi  19302  odmulg  19529  subgslw  19589  frgpnabllem1  19846  cyggeninv  19856  ablfaclem3  20062  lsslmod  20957  rhmpreimaidl  21277  psgnevpm  21571  pjff  21694  pjf2  21696  pjcss  21698  ocvpj  21699  evlslem3  22063  mhpdeg  22140  scmatscmid  22496  fvmptnn04ifc  22842  fvmptnn04ifd  22843  tgcl  22959  cldopn  23021  cncnp  23270  1stcelcls  23451  lly1stc  23486  refssex  23501  qtoptop2  23689  qtopid  23695  trfg  23881  flfneii  23982  fclsbas  24011  isfcf  24024  restutop  24227  restutopopn  24228  isucn2  24268  cfiluexsm  24279  cfilufg  24282  blgt0  24389  xblss2ps  24391  xblss2  24392  mopni  24482  metrest  24514  metustbl  24556  restmetu  24560  cfilss  25262  caun0  25273  cmetcaulem  25280  cfilresi  25287  cmetcusp  25346  cnlimci  25881  dvcl  25891  dvcnp  25911  dvcnp2  25912  dvnadd  25921  dvfsumrlimge0  26022  dvfsumrlim  26023  dvfsumrlim2  26024  fta1g  26160  plyeq0lem  26200  vieta1lem1  26301  vieta1lem2  26302  fsumharmonic  27000  dvdsflf1o  27175  dvdsflsumcom  27176  fsumvma  27201  vmadivsumb  27471  dchrisum0lem1a  27474  dchrisumlema  27476  dchrisumlem3  27479  dchrmusum2  27482  dchrvmasumlem2  27486  dchrvmasumiflem1  27489  dchrisum0fno1  27499  dchrisum0lem1b  27503  mulog2sumlem2  27523  vmalogdivsum2  27526  2vmadivsumlem  27528  selberglem2  27534  selbergb  27537  selberg2b  27540  selberg3lem1  27545  selberg4lem1  27548  pntpbnd1  27574  pntibndlem3  27580  pntlem3  27597  sltsleft  27877  sltsright  27878  cofcutr  27941  oppnid  28839  sspba  30823  sspg  30824  ssps  30826  sspn  30832  nmblore  30882  phpar  30920  ocorth  31387  elnlfn2  32025  foresf1o  32599  fnpreimac  32769  fpwrelmap  32832  elrgspnsubrunlem2  33336  kerunit  33415  0nellinds  33460  linds2eq  33471  dvdsruasso  33475  unitpidl1  33514  rhmpreimaprmidl  33541  mxidlirredi  33561  rprmdvds  33609  rprmnz  33610  1arithufdlem3  33636  ply1unit  33665  ply1degltlss  33686  selvply1rhmlema  33709  selvply1rhmlem1  33711  esplyfvaln  33765  exsslsb  33788  ply1degltdimlem  33813  lindsunlem  33815  dimkerim  33818  irngss  33878  0ringirng  33880  irngnminplynz  33903  algextdeglem8  33915  reff  34030  cnre2csqlem  34101  fmcncfil  34122  elzrhunit  34168  qqhval2lem  34172  baselsiga  34306  signsply0  34742  cvmliftmolem1  35510  mclsppslem  35812  mclspps  35813  fnetr  36580  relowlssretop  37726  mbfresfi  38034  itg2addnclem  38039  itg2addnclem2  38040  sstotbnd2  38142  rngoiso1o  38347  pridl  38405  lfli  39554  lkrf0  39586  cvrne  39774  atcvr0  39781  psubspi  40240  psubcli2N  40432  lhp1cvr  40492  lautle  40577  diadmleN  41531  sn-eluzp1l  42786  cvgdvgrat  44758  radcnvrat  44759  projf1o  45644  islptre  46065  islpcn  46083  icccncfext  46331  fdivmptf  49033  refdivmptf  49034  rege1logbrege0  49050  nelsubc2  49560  termcterm2  50005