Theorem simplbda 652

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

Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383

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 196  df-an 385

This theorem is referenced by:  cantnflem3  8471  fseqenlem2  8731  axdc3lem2  9156  fpwwe2lem12  9342  rlimsqzlem  14227  ramub1lem2  15569  invfun  16247  pltne  16785  cntzi  17585  odmulg  17796  subgslw  17854  frgpnabllem1  18099  cyggeninv  18108  ablfaclem3  18309  lsslmod  18781  evlslem3  19335  psgnevpm  19754  pjff  19875  pjf2  19877  pjcss  19879  ocvpj  19880  scmatscmid  20131  fvmptnn04ifc  20476  fvmptnn04ifd  20477  tgcl  20584  cldopn  20645  cncnp  20894  1stcelcls  21074  lly1stc  21109  refssex  21124  qtoptop2  21312  qtopid  21318  trfg  21505  flfneii  21606  fclsbas  21635  isfcf  21648  restutop  21851  restutopopn  21852  isucn2  21893  cfiluexsm  21904  cfilufg  21907  blgt0  22014  xblss2ps  22016  xblss2  22017  mopni  22107  metrest  22139  metustbl  22181  restmetu  22185  cfilss  22876  caun0  22887  cmetcaulem  22894  cfilresi  22901  cmetcusp  22958  cnlimci  23459  dvcl  23469  dvcnp  23488  dvcnp2  23489  dvnadd  23498  dvfsumrlimge0  23597  dvfsumrlim  23598  dvfsumrlim2  23599  fta1g  23731  plyeq0lem  23770  vieta1lem1  23869  vieta1lem2  23870  fsumharmonic  24538  dvdsflf1o  24713  dvdsflsumcom  24714  fsumvma  24738  vmadivsumb  24972  dchrisum0lem1a  24975  dchrisumlema  24977  dchrisumlem3  24980  dchrmusum2  24983  dchrvmasumlem2  24987  dchrvmasumiflem1  24990  dchrisum0fno1  25000  dchrisum0lem1b  25004  mulog2sumlem2  25024  vmalogdivsum2  25027  2vmadivsumlem  25029  selberglem2  25035  selbergb  25038  selberg2b  25041  selberg3lem1  25046  selberg4lem1  25049  pntpbnd1  25075  pntibndlem3  25081  pntlem3  25098  oppnid  25438  sspba  26966  sspg  26967  ssps  26969  sspn  26975  nmblore  27025  phpar  27063  ocorth  27534  elnlfn2  28172  foresf1o  28727  fpwrelmap  28896  kerunit  29154  reff  29234  cnre2csqlem  29284  fmcncfil  29305  elzrhunit  29351  qqhval2lem  29353  baselsiga  29505  signsply0  29954  cvmliftmolem1  30517  mclsppslem  30734  mclspps  30735  fnetr  31516  relowlssretop  32387  mbfresfi  32626  itg2addnclem  32631  itg2addnclem2  32632  sstotbnd2  32743  rngoiso1o  32948  pridl  33006  lfli  33366  lkrf0  33398  cvrne  33586  atcvr0  33593  psubspi  34051  psubcli2N  34243  lhp1cvr  34303  lautle  34388  diadmleN  35345  cvgdvgrat  37534  radcnvrat  37535  islptre  38686  islpcn  38706  icccncfext  38773  fdivmptf  42133  refdivmptf  42134  rege1logbrege0  42150