Theorem simplbda 499

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  cantnflem3  9601  fseqenlem2  9936  axdc3lem2  10362  fpwwe2lem11  10553  rlimsqzlem  15600  ramub1lem2  16987  invfun  17720  pltne  18287  cntzi  19293  odmulg  19520  subgslw  19580  frgpnabllem1  19837  cyggeninv  19847  ablfaclem3  20053  lsslmod  20944  rhmpreimaidl  21265  psgnevpm  21577  pjff  21700  pjf2  21702  pjcss  21704  ocvpj  21705  evlslem3  22067  mhpdeg  22120  scmatscmid  22480  fvmptnn04ifc  22826  fvmptnn04ifd  22827  tgcl  22943  cldopn  23005  cncnp  23254  1stcelcls  23435  lly1stc  23470  refssex  23485  qtoptop2  23673  qtopid  23679  trfg  23865  flfneii  23966  fclsbas  23995  isfcf  24008  restutop  24211  restutopopn  24212  isucn2  24252  cfiluexsm  24263  cfilufg  24266  blgt0  24373  xblss2ps  24375  xblss2  24376  mopni  24466  metrest  24498  metustbl  24540  restmetu  24544  cfilss  25246  caun0  25257  cmetcaulem  25264  cfilresi  25271  cmetcusp  25330  cnlimci  25865  dvcl  25875  dvcnp  25895  dvcnp2  25896  dvnadd  25905  dvfsumrlimge0  26009  dvfsumrlim  26010  dvfsumrlim2  26011  fta1g  26147  plyeq0lem  26187  vieta1lem1  26289  vieta1lem2  26290  fsumharmonic  26993  dvdsflf1o  27168  dvdsflsumcom  27169  fsumvma  27195  vmadivsumb  27465  dchrisum0lem1a  27468  dchrisumlema  27470  dchrisumlem3  27473  dchrmusum2  27476  dchrvmasumlem2  27480  dchrvmasumiflem1  27483  dchrisum0fno1  27493  dchrisum0lem1b  27497  mulog2sumlem2  27517  vmalogdivsum2  27520  2vmadivsumlem  27522  selberglem2  27528  selbergb  27531  selberg2b  27534  selberg3lem1  27539  selberg4lem1  27542  pntpbnd1  27568  pntibndlem3  27574  pntlem3  27591  sltsleft  27871  sltsright  27872  cofcutr  27935  oppnid  28833  sspba  30818  sspg  30819  ssps  30821  sspn  30827  nmblore  30877  phpar  30915  ocorth  31382  elnlfn2  32020  foresf1o  32594  fnpreimac  32763  fpwrelmap  32826  elrgspnsubrunlem2  33329  kerunit  33405  0nellinds  33450  linds2eq  33461  dvdsruasso  33465  unitpidl1  33504  rhmpreimaprmidl  33531  mxidlirredi  33551  rprmdvds  33599  rprmnz  33600  1arithufdlem3  33626  ply1unit  33655  ply1degltlss  33676  esplyfvaln  33738  exsslsb  33761  ply1degltdimlem  33787  lindsunlem  33789  dimkerim  33792  irngss  33852  0ringirng  33854  irngnminplynz  33877  algextdeglem8  33889  reff  34004  cnre2csqlem  34075  fmcncfil  34096  elzrhunit  34142  qqhval2lem  34146  baselsiga  34280  signsply0  34716  cvmliftmolem1  35484  mclsppslem  35786  mclspps  35787  fnetr  36554  relowlssretop  37690  mbfresfi  37998  itg2addnclem  38003  itg2addnclem2  38004  sstotbnd2  38106  rngoiso1o  38311  pridl  38369  lfli  39518  lkrf0  39550  cvrne  39738  atcvr0  39745  psubspi  40204  psubcli2N  40396  lhp1cvr  40456  lautle  40541  diadmleN  41495  sn-eluzp1l  42751  cvgdvgrat  44755  radcnvrat  44756  projf1o  45641  islptre  46064  islpcn  46082  icccncfext  46330  fdivmptf  49014  refdivmptf  49015  rege1logbrege0  49031  nelsubc2  49541  termcterm2  49986