Theorem simplbda 499

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  cantnflem3  9760  fseqenlem2  10094  axdc3lem2  10520  fpwwe2lem11  10710  rlimsqzlem  15697  ramub1lem2  17074  invfun  17825  pltne  18404  cntzi  19369  odmulg  19598  subgslw  19658  frgpnabllem1  19915  cyggeninv  19925  ablfaclem3  20131  lsslmod  20981  rhmpreimaidl  21310  psgnevpm  21630  pjff  21755  pjf2  21757  pjcss  21759  ocvpj  21760  evlslem3  22127  mhpdeg  22172  scmatscmid  22533  fvmptnn04ifc  22879  fvmptnn04ifd  22880  tgcl  22997  cldopn  23060  cncnp  23309  1stcelcls  23490  lly1stc  23525  refssex  23540  qtoptop2  23728  qtopid  23734  trfg  23920  flfneii  24021  fclsbas  24050  isfcf  24063  restutop  24267  restutopopn  24268  isucn2  24309  cfiluexsm  24320  cfilufg  24323  blgt0  24430  xblss2ps  24432  xblss2  24433  mopni  24526  metrest  24558  metustbl  24600  restmetu  24604  cfilss  25323  caun0  25334  cmetcaulem  25341  cfilresi  25348  cmetcusp  25407  cnlimci  25944  dvcl  25954  dvcnp  25974  dvcnp2  25975  dvcnp2OLD  25976  dvnadd  25985  dvfsumrlimge0  26091  dvfsumrlim  26092  dvfsumrlim2  26093  fta1g  26229  plyeq0lem  26269  vieta1lem1  26370  vieta1lem2  26371  fsumharmonic  27073  dvdsflf1o  27248  dvdsflsumcom  27249  fsumvma  27275  vmadivsumb  27545  dchrisum0lem1a  27548  dchrisumlema  27550  dchrisumlem3  27553  dchrmusum2  27556  dchrvmasumlem2  27560  dchrvmasumiflem1  27563  dchrisum0fno1  27573  dchrisum0lem1b  27577  mulog2sumlem2  27597  vmalogdivsum2  27600  2vmadivsumlem  27602  selberglem2  27608  selbergb  27611  selberg2b  27614  selberg3lem1  27619  selberg4lem1  27622  pntpbnd1  27648  pntibndlem3  27654  pntlem3  27671  ssltleft  27927  ssltright  27928  cofcutr  27976  oppnid  28772  sspba  30759  sspg  30760  ssps  30762  sspn  30768  nmblore  30818  phpar  30856  ocorth  31323  elnlfn2  31961  foresf1o  32532  fnpreimac  32689  fpwrelmap  32747  kerunit  33314  0nellinds  33363  linds2eq  33374  dvdsruasso  33378  unitpidl1  33417  rhmpreimaprmidl  33444  mxidlirredi  33464  rprmdvds  33512  rprmnz  33513  1arithufdlem3  33539  ply1unit  33565  ply1degltlss  33582  ply1degltdimlem  33635  lindsunlem  33637  dimkerim  33640  irngss  33687  0ringirng  33689  irngnminplynz  33705  algextdeglem8  33715  reff  33785  cnre2csqlem  33856  fmcncfil  33877  elzrhunit  33925  qqhval2lem  33927  baselsiga  34079  signsply0  34528  cvmliftmolem1  35249  mclsppslem  35551  mclspps  35552  fnetr  36317  relowlssretop  37329  mbfresfi  37626  itg2addnclem  37631  itg2addnclem2  37632  sstotbnd2  37734  rngoiso1o  37939  pridl  37997  lfli  39017  lkrf0  39049  cvrne  39237  atcvr0  39244  psubspi  39704  psubcli2N  39896  lhp1cvr  39956  lautle  40041  diadmleN  40995  sn-eluzp1l  42296  cvgdvgrat  44282  radcnvrat  44283  projf1o  45104  islptre  45540  islpcn  45560  icccncfext  45808  fdivmptf  48275  refdivmptf  48276  rege1logbrege0  48292