Theorem simplbda 500

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

Hypothesis

Ref	Expression
pm3.26bda.1	⊢ (𝜑 → (𝜓 ↔ (𝜒 ∧ 𝜃)))

Assertion

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

Proof of Theorem simplbda

Step	Hyp	Ref	Expression
1		pm3.26bda.1	. . 3 ⊢ (𝜑 → (𝜓 ↔ (𝜒 ∧ 𝜃)))
2	1	biimpa 477	. 2 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 ∧ 𝜃))
3	2	simprd 496	1 ⊢ ((𝜑 ∧ 𝜓) → 𝜃)

Syntax hints:   → wi 4   ↔ wb 205   ∧ 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 206  df-an 397

This theorem is referenced by:  cantnflem3  9458  fseqenlem2  9790  axdc3lem2  10216  fpwwe2lem11  10406  rlimsqzlem  15369  ramub1lem2  16737  invfun  17485  pltne  18061  cntzi  18944  odmulg  19172  subgslw  19230  frgpnabllem1  19483  cyggeninv  19492  ablfaclem3  19699  lsslmod  20231  psgnevpm  20803  pjff  20928  pjf2  20930  pjcss  20932  ocvpj  20933  evlslem3  21299  mhpdeg  21344  scmatscmid  21664  fvmptnn04ifc  22010  fvmptnn04ifd  22011  tgcl  22128  cldopn  22191  cncnp  22440  1stcelcls  22621  lly1stc  22656  refssex  22671  qtoptop2  22859  qtopid  22865  trfg  23051  flfneii  23152  fclsbas  23181  isfcf  23194  restutop  23398  restutopopn  23399  isucn2  23440  cfiluexsm  23451  cfilufg  23454  blgt0  23561  xblss2ps  23563  xblss2  23564  mopni  23657  metrest  23689  metustbl  23731  restmetu  23735  cfilss  24443  caun0  24454  cmetcaulem  24461  cfilresi  24468  cmetcusp  24527  cnlimci  25062  dvcl  25072  dvcnp  25092  dvcnp2  25093  dvnadd  25102  dvfsumrlimge0  25203  dvfsumrlim  25204  dvfsumrlim2  25205  fta1g  25341  plyeq0lem  25380  vieta1lem1  25479  vieta1lem2  25480  fsumharmonic  26170  dvdsflf1o  26345  dvdsflsumcom  26346  fsumvma  26370  vmadivsumb  26640  dchrisum0lem1a  26643  dchrisumlema  26645  dchrisumlem3  26648  dchrmusum2  26651  dchrvmasumlem2  26655  dchrvmasumiflem1  26658  dchrisum0fno1  26668  dchrisum0lem1b  26672  mulog2sumlem2  26692  vmalogdivsum2  26695  2vmadivsumlem  26697  selberglem2  26703  selbergb  26706  selberg2b  26709  selberg3lem1  26714  selberg4lem1  26717  pntpbnd1  26743  pntibndlem3  26749  pntlem3  26766  oppnid  27116  sspba  29098  sspg  29099  ssps  29101  sspn  29107  nmblore  29157  phpar  29195  ocorth  29662  elnlfn2  30300  foresf1o  30859  fnpreimac  31017  fpwrelmap  31077  kerunit  31531  0nellinds  31575  linds2eq  31584  rhmpreimaidl  31612  rhmpreimaprmidl  31636  lindsunlem  31714  dimkerim  31717  reff  31798  cnre2csqlem  31869  fmcncfil  31890  elzrhunit  31938  qqhval2lem  31940  baselsiga  32092  signsply0  32539  cvmliftmolem1  33252  mclsppslem  33554  mclspps  33555  ssltleft  34063  ssltright  34064  cofcutr  34101  fnetr  34549  relowlssretop  35543  mbfresfi  35832  itg2addnclem  35837  itg2addnclem2  35838  sstotbnd2  35941  rngoiso1o  36146  pridl  36204  lfli  37082  lkrf0  37114  cvrne  37302  atcvr0  37309  psubspi  37768  psubcli2N  37960  lhp1cvr  38020  lautle  38105  diadmleN  39059  cvgdvgrat  41938  radcnvrat  41939  projf1o  42743  islptre  43167  islpcn  43187  icccncfext  43435  fdivmptf  45898  refdivmptf  45899  rege1logbrege0  45915