Theorem simplbda 498

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 394

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 206  df-an 395

This theorem is referenced by:  cantnflem3  9688  fseqenlem2  10022  axdc3lem2  10448  fpwwe2lem11  10638  rlimsqzlem  15599  ramub1lem2  16964  invfun  17715  pltne  18291  cntzi  19234  odmulg  19465  subgslw  19525  frgpnabllem1  19782  cyggeninv  19792  ablfaclem3  19998  lsslmod  20715  psgnevpm  21361  pjff  21486  pjf2  21488  pjcss  21490  ocvpj  21491  evlslem3  21862  mhpdeg  21907  scmatscmid  22228  fvmptnn04ifc  22574  fvmptnn04ifd  22575  tgcl  22692  cldopn  22755  cncnp  23004  1stcelcls  23185  lly1stc  23220  refssex  23235  qtoptop2  23423  qtopid  23429  trfg  23615  flfneii  23716  fclsbas  23745  isfcf  23758  restutop  23962  restutopopn  23963  isucn2  24004  cfiluexsm  24015  cfilufg  24018  blgt0  24125  xblss2ps  24127  xblss2  24128  mopni  24221  metrest  24253  metustbl  24295  restmetu  24299  cfilss  25018  caun0  25029  cmetcaulem  25036  cfilresi  25043  cmetcusp  25102  cnlimci  25638  dvcl  25648  dvcnp  25668  dvcnp2  25669  dvcnp2OLD  25670  dvnadd  25679  dvfsumrlimge0  25782  dvfsumrlim  25783  dvfsumrlim2  25784  fta1g  25920  plyeq0lem  25959  vieta1lem1  26059  vieta1lem2  26060  fsumharmonic  26752  dvdsflf1o  26927  dvdsflsumcom  26928  fsumvma  26952  vmadivsumb  27222  dchrisum0lem1a  27225  dchrisumlema  27227  dchrisumlem3  27230  dchrmusum2  27233  dchrvmasumlem2  27237  dchrvmasumiflem1  27240  dchrisum0fno1  27250  dchrisum0lem1b  27254  mulog2sumlem2  27274  vmalogdivsum2  27277  2vmadivsumlem  27279  selberglem2  27285  selbergb  27288  selberg2b  27291  selberg3lem1  27296  selberg4lem1  27299  pntpbnd1  27325  pntibndlem3  27331  pntlem3  27348  ssltleft  27602  ssltright  27603  cofcutr  27649  oppnid  28264  sspba  30247  sspg  30248  ssps  30250  sspn  30256  nmblore  30306  phpar  30344  ocorth  30811  elnlfn2  31449  foresf1o  32009  fnpreimac  32163  fpwrelmap  32225  kerunit  32707  0nellinds  32757  dvdsruasso  32764  linds2eq  32771  rhmpreimaidl  32811  unitpidl1  32816  rhmpreimaprmidl  32844  mxidlirredi  32861  ply1degltlss  32942  ply1degltdimlem  32995  lindsunlem  32997  dimkerim  33000  irngss  33040  0ringirng  33042  irngnminplynz  33060  algextdeglem8  33069  reff  33117  cnre2csqlem  33188  fmcncfil  33209  elzrhunit  33257  qqhval2lem  33259  baselsiga  33411  signsply0  33860  cvmliftmolem1  34570  mclsppslem  34872  mclspps  34873  fnetr  35539  relowlssretop  36547  mbfresfi  36837  itg2addnclem  36842  itg2addnclem2  36843  sstotbnd2  36945  rngoiso1o  37150  pridl  37208  lfli  38234  lkrf0  38266  cvrne  38454  atcvr0  38461  psubspi  38921  psubcli2N  39113  lhp1cvr  39173  lautle  39258  diadmleN  40212  cvgdvgrat  43374  radcnvrat  43375  projf1o  44194  islptre  44633  islpcn  44653  icccncfext  44901  fdivmptf  47314  refdivmptf  47315  rege1logbrege0  47331