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  9147  fseqenlem2  9444  axdc3lem2  9866  fpwwe2lem12  10056  rlimsqzlem  15000  ramub1lem2  16358  invfun  17029  pltne  17567  cntzi  18454  odmulg  18678  subgslw  18736  frgpnabllem1  18988  cyggeninv  18997  ablfaclem3  19204  lsslmod  19727  evlslem3  20288  mhpdeg  20331  psgnevpm  20728  pjff  20851  pjf2  20853  pjcss  20855  ocvpj  20856  scmatscmid  21110  fvmptnn04ifc  21455  fvmptnn04ifd  21456  tgcl  21572  cldopn  21634  cncnp  21883  1stcelcls  22064  lly1stc  22099  refssex  22114  qtoptop2  22302  qtopid  22308  trfg  22494  flfneii  22595  fclsbas  22624  isfcf  22637  restutop  22841  restutopopn  22842  isucn2  22883  cfiluexsm  22894  cfilufg  22897  blgt0  23004  xblss2ps  23006  xblss2  23007  mopni  23097  metrest  23129  metustbl  23171  restmetu  23175  cfilss  23868  caun0  23879  cmetcaulem  23886  cfilresi  23893  cmetcusp  23952  cnlimci  24484  dvcl  24494  dvcnp  24513  dvcnp2  24514  dvnadd  24523  dvfsumrlimge0  24624  dvfsumrlim  24625  dvfsumrlim2  24626  fta1g  24759  plyeq0lem  24798  vieta1lem1  24897  vieta1lem2  24898  fsumharmonic  25587  dvdsflf1o  25762  dvdsflsumcom  25763  fsumvma  25787  vmadivsumb  26057  dchrisum0lem1a  26060  dchrisumlema  26062  dchrisumlem3  26065  dchrmusum2  26068  dchrvmasumlem2  26072  dchrvmasumiflem1  26075  dchrisum0fno1  26085  dchrisum0lem1b  26089  mulog2sumlem2  26109  vmalogdivsum2  26112  2vmadivsumlem  26114  selberglem2  26120  selbergb  26123  selberg2b  26126  selberg3lem1  26131  selberg4lem1  26134  pntpbnd1  26160  pntibndlem3  26166  pntlem3  26183  oppnid  26530  sspba  28502  sspg  28503  ssps  28505  sspn  28511  nmblore  28561  phpar  28599  ocorth  29066  elnlfn2  29704  foresf1o  30264  fnpreimac  30416  fpwrelmap  30469  kerunit  30917  0nellinds  30956  linds2eq  30963  lindsunlem  31044  dimkerim  31047  reff  31127  cnre2csqlem  31174  fmcncfil  31195  elzrhunit  31241  qqhval2lem  31243  baselsiga  31395  signsply0  31842  cvmliftmolem1  32549  mclsppslem  32851  mclspps  32852  fnetr  33720  relowlssretop  34668  mbfresfi  34973  itg2addnclem  34978  itg2addnclem2  34979  sstotbnd2  35085  rngoiso1o  35290  pridl  35348  lfli  36230  lkrf0  36262  cvrne  36450  atcvr0  36457  psubspi  36916  psubcli2N  37108  lhp1cvr  37168  lautle  37253  diadmleN  38207  cvgdvgrat  40719  radcnvrat  40720  projf1o  41533  islptre  41974  islpcn  41994  icccncfext  42244  fdivmptf  44675  refdivmptf  44676  rege1logbrege0  44692