Theorem simplbda 503

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399

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 210  df-an 400

This theorem is referenced by:  cantnflem3  9284  fseqenlem2  9604  axdc3lem2  10030  fpwwe2lem11  10220  rlimsqzlem  15177  ramub1lem2  16543  invfun  17223  pltne  17794  cntzi  18677  odmulg  18901  subgslw  18959  frgpnabllem1  19212  cyggeninv  19221  ablfaclem3  19428  lsslmod  19951  psgnevpm  20505  pjff  20628  pjf2  20630  pjcss  20632  ocvpj  20633  evlslem3  20994  mhpdeg  21039  scmatscmid  21357  fvmptnn04ifc  21703  fvmptnn04ifd  21704  tgcl  21820  cldopn  21882  cncnp  22131  1stcelcls  22312  lly1stc  22347  refssex  22362  qtoptop2  22550  qtopid  22556  trfg  22742  flfneii  22843  fclsbas  22872  isfcf  22885  restutop  23089  restutopopn  23090  isucn2  23130  cfiluexsm  23141  cfilufg  23144  blgt0  23251  xblss2ps  23253  xblss2  23254  mopni  23344  metrest  23376  metustbl  23418  restmetu  23422  cfilss  24121  caun0  24132  cmetcaulem  24139  cfilresi  24146  cmetcusp  24205  cnlimci  24740  dvcl  24750  dvcnp  24770  dvcnp2  24771  dvnadd  24780  dvfsumrlimge0  24881  dvfsumrlim  24882  dvfsumrlim2  24883  fta1g  25019  plyeq0lem  25058  vieta1lem1  25157  vieta1lem2  25158  fsumharmonic  25848  dvdsflf1o  26023  dvdsflsumcom  26024  fsumvma  26048  vmadivsumb  26318  dchrisum0lem1a  26321  dchrisumlema  26323  dchrisumlem3  26326  dchrmusum2  26329  dchrvmasumlem2  26333  dchrvmasumiflem1  26336  dchrisum0fno1  26346  dchrisum0lem1b  26350  mulog2sumlem2  26370  vmalogdivsum2  26373  2vmadivsumlem  26375  selberglem2  26381  selbergb  26384  selberg2b  26387  selberg3lem1  26392  selberg4lem1  26395  pntpbnd1  26421  pntibndlem3  26427  pntlem3  26444  oppnid  26791  sspba  28762  sspg  28763  ssps  28765  sspn  28771  nmblore  28821  phpar  28859  ocorth  29326  elnlfn2  29964  foresf1o  30523  fnpreimac  30682  fpwrelmap  30742  kerunit  31195  0nellinds  31234  linds2eq  31243  rhmpreimaidl  31271  rhmpreimaprmidl  31295  lindsunlem  31373  dimkerim  31376  reff  31457  cnre2csqlem  31528  fmcncfil  31549  elzrhunit  31595  qqhval2lem  31597  baselsiga  31749  signsply0  32196  cvmliftmolem1  32910  mclsppslem  33212  mclspps  33213  ssltleft  33740  ssltright  33741  cofcutr  33778  fnetr  34226  relowlssretop  35220  mbfresfi  35509  itg2addnclem  35514  itg2addnclem2  35515  sstotbnd2  35618  rngoiso1o  35823  pridl  35881  lfli  36761  lkrf0  36793  cvrne  36981  atcvr0  36988  psubspi  37447  psubcli2N  37639  lhp1cvr  37699  lautle  37784  diadmleN  38738  cvgdvgrat  41545  radcnvrat  41546  projf1o  42350  islptre  42778  islpcn  42798  icccncfext  43046  fdivmptf  45503  refdivmptf  45504  rege1logbrege0  45520