Theorem simplbda 500

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

Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  cantnflem3  9000  fseqenlem2  9297  axdc3lem2  9719  fpwwe2lem12  9909  rlimsqzlem  14839  ramub1lem2  16192  invfun  16863  pltne  17401  cntzi  18200  odmulg  18413  subgslw  18471  frgpnabllem1  18716  cyggeninv  18725  ablfaclem3  18926  lsslmod  19422  evlslem3  19981  mhpdeg  20019  psgnevpm  20415  pjff  20538  pjf2  20540  pjcss  20542  ocvpj  20543  scmatscmid  20799  fvmptnn04ifc  21144  fvmptnn04ifd  21145  tgcl  21261  cldopn  21323  cncnp  21572  1stcelcls  21753  lly1stc  21788  refssex  21803  qtoptop2  21991  qtopid  21997  trfg  22183  flfneii  22284  fclsbas  22313  isfcf  22326  restutop  22529  restutopopn  22530  isucn2  22571  cfiluexsm  22582  cfilufg  22585  blgt0  22692  xblss2ps  22694  xblss2  22695  mopni  22785  metrest  22817  metustbl  22859  restmetu  22863  cfilss  23556  caun0  23567  cmetcaulem  23574  cfilresi  23581  cmetcusp  23640  cnlimci  24170  dvcl  24180  dvcnp  24199  dvcnp2  24200  dvnadd  24209  dvfsumrlimge0  24310  dvfsumrlim  24311  dvfsumrlim2  24312  fta1g  24444  plyeq0lem  24483  vieta1lem1  24582  vieta1lem2  24583  fsumharmonic  25271  dvdsflf1o  25446  dvdsflsumcom  25447  fsumvma  25471  vmadivsumb  25741  dchrisum0lem1a  25744  dchrisumlema  25746  dchrisumlem3  25749  dchrmusum2  25752  dchrvmasumlem2  25756  dchrvmasumiflem1  25759  dchrisum0fno1  25769  dchrisum0lem1b  25773  mulog2sumlem2  25793  vmalogdivsum2  25796  2vmadivsumlem  25798  selberglem2  25804  selbergb  25807  selberg2b  25810  selberg3lem1  25815  selberg4lem1  25818  pntpbnd1  25844  pntibndlem3  25850  pntlem3  25867  oppnid  26214  sspba  28195  sspg  28196  ssps  28198  sspn  28204  nmblore  28254  phpar  28292  ocorth  28759  elnlfn2  29397  foresf1o  29957  fnpreimac  30106  fpwrelmap  30157  kerunit  30550  0nellinds  30583  linds2eq  30587  lindsunlem  30624  dimkerim  30627  reff  30720  cnre2csqlem  30770  fmcncfil  30791  elzrhunit  30837  qqhval2lem  30839  baselsiga  30991  signsply0  31438  cvmliftmolem1  32136  mclsppslem  32438  mclspps  32439  fnetr  33308  relowlssretop  34175  mbfresfi  34469  itg2addnclem  34474  itg2addnclem2  34475  sstotbnd2  34584  rngoiso1o  34789  pridl  34847  lfli  35728  lkrf0  35760  cvrne  35948  atcvr0  35955  psubspi  36414  psubcli2N  36606  lhp1cvr  36666  lautle  36751  diadmleN  37705  cvgdvgrat  40183  radcnvrat  40184  projf1o  40999  islptre  41442  islpcn  41462  icccncfext  41711  fdivmptf  44082  refdivmptf  44083  rege1logbrege0  44099