Theorem simplbda 504

Description: Deduction eliminating a conjunct. (Contributed by NM, 22-Oct-2007.)

Hypothesis

Ref	Expression
simplbda.1	⊢ (𝜑 → (𝜓 ↔ (𝜒 ∧ 𝜃)))

Assertion

Ref	Expression
simplbda	⊢ ((𝜑 ∧ 𝜓) → 𝜃)

Proof of Theorem simplbda

Step	Hyp	Ref	Expression
1		simplbda.1	. . 3 ⊢ (𝜑 → (𝜓 ↔ (𝜒 ∧ 𝜃)))
2	1	biimpa 481	. 2 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 ∧ 𝜃))
3	2	simprd 500	1 ⊢ ((𝜑 ∧ 𝜓) → 𝜃)

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 400

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 401

This theorem is used by:  cantnflem3  9658  fseqenlem2  10016  axdc3lem2  10441  fpwwe2lem11  10632  rlimsqzlem  15707  ramub1lem2  17093  invfun  17827  pltne  18394  cntzi  19405  odmulg  19632  subgslw  19692  frgpnabllem1  19949  cyggeninv  19959  ablfaclem3  20165  lsslmod  21092  rhmpreimaidl  21427  rhmpreimaprmidl  21490  psgnevpm  21750  pjff  21873  pjf2  21875  pjcss  21877  ocvpj  21878  evlslem3  22242  mhpdeg  22319  scmatscmid  22674  fvmptnn04ifc  23020  fvmptnn04ifd  23021  tgcl  23137  cldopn  23199  cncnp  23448  1stcelcls  23629  lly1stc  23664  refssex  23679  qtoptop2  23867  qtopid  23873  trfg  24059  flfneii  24160  fclsbas  24189  isfcf  24202  restutop  24405  restutopopn  24406  isucn2  24446  cfiluexsm  24457  cfilufg  24460  blgt0  24567  xblss2ps  24569  xblss2  24570  mopni  24660  metrest  24692  metustbl  24734  restmetu  24738  cfilss  25440  caun0  25451  cmetcaulem  25458  cfilresi  25465  cmetcusp  25524  cnlimci  26059  dvcl  26069  dvcnp  26089  dvcnp2  26090  dvnadd  26099  dvfsumrlimge0  26200  dvfsumrlim  26201  dvfsumrlim2  26202  fta1g  26338  plyeq0lem  26378  vieta1lem1  26482  vieta1lem2  26483  fsumharmonic  27187  dvdsflf1o  27362  dvdsflsumcom  27363  fsumvma  27388  vmadivsumb  27658  dchrisum0lem1a  27661  dchrisumlema  27663  dchrisumlem3  27666  dchrmusum2  27669  dchrvmasumlem2  27673  dchrvmasumiflem1  27676  dchrisum0fno1  27686  dchrisum0lem1b  27690  mulog2sumlem2  27710  vmalogdivsum2  27713  2vmadivsumlem  27715  selberglem2  27721  selbergb  27724  selberg2b  27727  selberg3lem1  27732  selberg4lem1  27735  pntpbnd1  27761  pntibndlem3  27767  pntlem3  27784  sltsleft  28064  sltsright  28065  cofcutr  28128  oppnid  29038  prlnghpg  29207  sspba  31090  sspg  31091  ssps  31093  sspn  31099  nmblore  31149  phpar  31187  ocorth  31654  elnlfn2  32292  foresf1o  32861  fnpreimac  33026  fpwrelmap  33089  elrgspnsubrunlem2  33577  kerunit  33654  0nellinds  33694  linds2eq  33703  dvdsruasso  33707  unitpidl1  33741  mxidlirredi  33763  dflringlem2  33794  rprmdvds  33818  rprmnz  33819  1arithufdlem3  33845  ply1unit  33874  ply1degltlss  33895  selvply1rhmlema  33917  selvply1rhmlem1  33919  esplyfvaln  33973  exsslsb  33996  ply1degltdimlem  34021  lindsunlem  34023  dimkerim  34026  irngss  34086  0ringirng  34088  irngnminplynz  34111  algextdeglem8  34123  reff  34238  cnre2csqlem  34309  fmcncfil  34330  elzrhunit  34376  qqhval2lem  34380  baselsiga  34514  signsply0  34947  cvmliftmolem1  35781  mclsppslem  36083  mclspps  36084  fnetr  36890  relowlssretop  38037  mbfresfi  38345  itg2addnclem  38350  itg2addnclem2  38351  sstotbnd2  38453  rngoiso1o  38658  pridl  38716  lfli  39863  lkrf0  39895  cvrne  40083  atcvr0  40090  psubspi  40549  psubcli2N  40741  lhp1cvr  40801  lautle  40886  diadmleN  41840  sn-eluzp1l  43097  cvgdvgrat  45051  radcnvrat  45052  projf1o  45942  islptre  46363  islpcn  46381  icccncfext  46629  fdivmptf  49349  refdivmptf  49350  rege1logbrege0  49366  nelsubc2  49875  termcterm2  50320