Theorem simplbda 499

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

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

This theorem is referenced by:  cantnflem3  9379  fseqenlem2  9712  axdc3lem2  10138  fpwwe2lem11  10328  rlimsqzlem  15288  ramub1lem2  16656  invfun  17393  pltne  17967  cntzi  18850  odmulg  19078  subgslw  19136  frgpnabllem1  19389  cyggeninv  19398  ablfaclem3  19605  lsslmod  20137  psgnevpm  20706  pjff  20829  pjf2  20831  pjcss  20833  ocvpj  20834  evlslem3  21200  mhpdeg  21245  scmatscmid  21563  fvmptnn04ifc  21909  fvmptnn04ifd  21910  tgcl  22027  cldopn  22090  cncnp  22339  1stcelcls  22520  lly1stc  22555  refssex  22570  qtoptop2  22758  qtopid  22764  trfg  22950  flfneii  23051  fclsbas  23080  isfcf  23093  restutop  23297  restutopopn  23298  isucn2  23339  cfiluexsm  23350  cfilufg  23353  blgt0  23460  xblss2ps  23462  xblss2  23463  mopni  23554  metrest  23586  metustbl  23628  restmetu  23632  cfilss  24339  caun0  24350  cmetcaulem  24357  cfilresi  24364  cmetcusp  24423  cnlimci  24958  dvcl  24968  dvcnp  24988  dvcnp2  24989  dvnadd  24998  dvfsumrlimge0  25099  dvfsumrlim  25100  dvfsumrlim2  25101  fta1g  25237  plyeq0lem  25276  vieta1lem1  25375  vieta1lem2  25376  fsumharmonic  26066  dvdsflf1o  26241  dvdsflsumcom  26242  fsumvma  26266  vmadivsumb  26536  dchrisum0lem1a  26539  dchrisumlema  26541  dchrisumlem3  26544  dchrmusum2  26547  dchrvmasumlem2  26551  dchrvmasumiflem1  26554  dchrisum0fno1  26564  dchrisum0lem1b  26568  mulog2sumlem2  26588  vmalogdivsum2  26591  2vmadivsumlem  26593  selberglem2  26599  selbergb  26602  selberg2b  26605  selberg3lem1  26610  selberg4lem1  26613  pntpbnd1  26639  pntibndlem3  26645  pntlem3  26662  oppnid  27011  sspba  28990  sspg  28991  ssps  28993  sspn  28999  nmblore  29049  phpar  29087  ocorth  29554  elnlfn2  30192  foresf1o  30751  fnpreimac  30910  fpwrelmap  30970  kerunit  31424  0nellinds  31468  linds2eq  31477  rhmpreimaidl  31505  rhmpreimaprmidl  31529  lindsunlem  31607  dimkerim  31610  reff  31691  cnre2csqlem  31762  fmcncfil  31783  elzrhunit  31829  qqhval2lem  31831  baselsiga  31983  signsply0  32430  cvmliftmolem1  33143  mclsppslem  33445  mclspps  33446  ssltleft  33981  ssltright  33982  cofcutr  34019  fnetr  34467  relowlssretop  35461  mbfresfi  35750  itg2addnclem  35755  itg2addnclem2  35756  sstotbnd2  35859  rngoiso1o  36064  pridl  36122  lfli  37002  lkrf0  37034  cvrne  37222  atcvr0  37229  psubspi  37688  psubcli2N  37880  lhp1cvr  37940  lautle  38025  diadmleN  38979  cvgdvgrat  41820  radcnvrat  41821  projf1o  42625  islptre  43050  islpcn  43070  icccncfext  43318  fdivmptf  45775  refdivmptf  45776  rege1logbrege0  45792