Theorem simplbda 501

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 397

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 398

This theorem is referenced by:  cantnflem3  9686  fseqenlem2  10020  axdc3lem2  10446  fpwwe2lem11  10636  rlimsqzlem  15595  ramub1lem2  16960  invfun  17711  pltne  18287  cntzi  19193  odmulg  19424  subgslw  19484  frgpnabllem1  19741  cyggeninv  19751  ablfaclem3  19957  lsslmod  20571  psgnevpm  21142  pjff  21267  pjf2  21269  pjcss  21271  ocvpj  21272  evlslem3  21643  mhpdeg  21688  scmatscmid  22008  fvmptnn04ifc  22354  fvmptnn04ifd  22355  tgcl  22472  cldopn  22535  cncnp  22784  1stcelcls  22965  lly1stc  23000  refssex  23015  qtoptop2  23203  qtopid  23209  trfg  23395  flfneii  23496  fclsbas  23525  isfcf  23538  restutop  23742  restutopopn  23743  isucn2  23784  cfiluexsm  23795  cfilufg  23798  blgt0  23905  xblss2ps  23907  xblss2  23908  mopni  24001  metrest  24033  metustbl  24075  restmetu  24079  cfilss  24787  caun0  24798  cmetcaulem  24805  cfilresi  24812  cmetcusp  24871  cnlimci  25406  dvcl  25416  dvcnp  25436  dvcnp2  25437  dvnadd  25446  dvfsumrlimge0  25547  dvfsumrlim  25548  dvfsumrlim2  25549  fta1g  25685  plyeq0lem  25724  vieta1lem1  25823  vieta1lem2  25824  fsumharmonic  26516  dvdsflf1o  26691  dvdsflsumcom  26692  fsumvma  26716  vmadivsumb  26986  dchrisum0lem1a  26989  dchrisumlema  26991  dchrisumlem3  26994  dchrmusum2  26997  dchrvmasumlem2  27001  dchrvmasumiflem1  27004  dchrisum0fno1  27014  dchrisum0lem1b  27018  mulog2sumlem2  27038  vmalogdivsum2  27041  2vmadivsumlem  27043  selberglem2  27049  selbergb  27052  selberg2b  27055  selberg3lem1  27060  selberg4lem1  27063  pntpbnd1  27089  pntibndlem3  27095  pntlem3  27112  ssltleft  27365  ssltright  27366  cofcutr  27411  oppnid  27997  sspba  29980  sspg  29981  ssps  29983  sspn  29989  nmblore  30039  phpar  30077  ocorth  30544  elnlfn2  31182  foresf1o  31742  fnpreimac  31896  fpwrelmap  31958  kerunit  32437  0nellinds  32483  dvdsruasso  32490  linds2eq  32497  rhmpreimaidl  32537  unitpidl1  32542  rhmpreimaprmidl  32570  mxidlirredi  32587  ply1degltlss  32667  ply1degltdimlem  32707  lindsunlem  32709  dimkerim  32712  irngss  32751  0ringirng  32753  irngnminplynz  32771  reff  32819  cnre2csqlem  32890  fmcncfil  32911  elzrhunit  32959  qqhval2lem  32961  baselsiga  33113  signsply0  33562  cvmliftmolem1  34272  mclsppslem  34574  mclspps  34575  gg-dvcnp2  35174  fnetr  35236  relowlssretop  36244  mbfresfi  36534  itg2addnclem  36539  itg2addnclem2  36540  sstotbnd2  36642  rngoiso1o  36847  pridl  36905  lfli  37931  lkrf0  37963  cvrne  38151  atcvr0  38158  psubspi  38618  psubcli2N  38810  lhp1cvr  38870  lautle  38955  diadmleN  39909  cvgdvgrat  43072  radcnvrat  43073  projf1o  43896  islptre  44335  islpcn  44355  icccncfext  44603  fdivmptf  47227  refdivmptf  47228  rege1logbrege0  47244