Theorem simplbda 502

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  cantnflem3  9156  fseqenlem2  9453  axdc3lem2  9875  fpwwe2lem12  10065  rlimsqzlem  15007  ramub1lem2  16365  invfun  17036  pltne  17574  cntzi  18461  odmulg  18685  subgslw  18743  frgpnabllem1  18995  cyggeninv  19004  ablfaclem3  19211  lsslmod  19734  evlslem3  20295  mhpdeg  20338  psgnevpm  20735  pjff  20858  pjf2  20860  pjcss  20862  ocvpj  20863  scmatscmid  21117  fvmptnn04ifc  21462  fvmptnn04ifd  21463  tgcl  21579  cldopn  21641  cncnp  21890  1stcelcls  22071  lly1stc  22106  refssex  22121  qtoptop2  22309  qtopid  22315  trfg  22501  flfneii  22602  fclsbas  22631  isfcf  22644  restutop  22848  restutopopn  22849  isucn2  22890  cfiluexsm  22901  cfilufg  22904  blgt0  23011  xblss2ps  23013  xblss2  23014  mopni  23104  metrest  23136  metustbl  23178  restmetu  23182  cfilss  23875  caun0  23886  cmetcaulem  23893  cfilresi  23900  cmetcusp  23959  cnlimci  24489  dvcl  24499  dvcnp  24518  dvcnp2  24519  dvnadd  24528  dvfsumrlimge0  24629  dvfsumrlim  24630  dvfsumrlim2  24631  fta1g  24763  plyeq0lem  24802  vieta1lem1  24901  vieta1lem2  24902  fsumharmonic  25591  dvdsflf1o  25766  dvdsflsumcom  25767  fsumvma  25791  vmadivsumb  26061  dchrisum0lem1a  26064  dchrisumlema  26066  dchrisumlem3  26069  dchrmusum2  26072  dchrvmasumlem2  26076  dchrvmasumiflem1  26079  dchrisum0fno1  26089  dchrisum0lem1b  26093  mulog2sumlem2  26113  vmalogdivsum2  26116  2vmadivsumlem  26118  selberglem2  26124  selbergb  26127  selberg2b  26130  selberg3lem1  26135  selberg4lem1  26138  pntpbnd1  26164  pntibndlem3  26170  pntlem3  26187  oppnid  26534  sspba  28506  sspg  28507  ssps  28509  sspn  28515  nmblore  28565  phpar  28603  ocorth  29070  elnlfn2  29708  foresf1o  30267  fnpreimac  30418  fpwrelmap  30471  kerunit  30898  0nellinds  30937  linds2eq  30943  lindsunlem  31022  dimkerim  31025  reff  31105  cnre2csqlem  31155  fmcncfil  31176  elzrhunit  31222  qqhval2lem  31224  baselsiga  31376  signsply0  31823  cvmliftmolem1  32530  mclsppslem  32832  mclspps  32833  fnetr  33701  relowlssretop  34646  mbfresfi  34940  itg2addnclem  34945  itg2addnclem2  34946  sstotbnd2  35054  rngoiso1o  35259  pridl  35317  lfli  36199  lkrf0  36231  cvrne  36419  atcvr0  36426  psubspi  36885  psubcli2N  37077  lhp1cvr  37137  lautle  37222  diadmleN  38176  cvgdvgrat  40652  radcnvrat  40653  projf1o  41466  islptre  41907  islpcn  41927  icccncfext  42177  fdivmptf  44608  refdivmptf  44609  rege1logbrege0  44625