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 ⊢ ((𝜑 ∧ 𝜓) → 𝜃)

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  cantnflem3  9648  fseqenlem2  9997  axdc3lem2  10423  fpwwe2lem11  10614  rlimsqzlem  15690  ramub1lem2  17077  invfun  17811  pltne  18378  cntzi  19390  odmulg  19617  subgslw  19677  frgpnabllem1  19934  cyggeninv  19944  ablfaclem3  20150  lsslmod  21050  rhmpreimaidl  21378  rhmpreimaprmidl  21439  psgnevpm  21699  pjff  21822  pjf2  21824  pjcss  21826  ocvpj  21827  evlslem3  22191  mhpdeg  22268  scmatscmid  22624  fvmptnn04ifc  22970  fvmptnn04ifd  22971  tgcl  23087  cldopn  23149  cncnp  23398  1stcelcls  23579  lly1stc  23614  refssex  23629  qtoptop2  23817  qtopid  23823  trfg  24009  flfneii  24110  fclsbas  24139  isfcf  24152  restutop  24355  restutopopn  24356  isucn2  24396  cfiluexsm  24407  cfilufg  24410  blgt0  24517  xblss2ps  24519  xblss2  24520  mopni  24610  metrest  24642  metustbl  24684  restmetu  24688  cfilss  25390  caun0  25401  cmetcaulem  25408  cfilresi  25415  cmetcusp  25474  cnlimci  26009  dvcl  26019  dvcnp  26039  dvcnp2  26040  dvnadd  26049  dvfsumrlimge0  26150  dvfsumrlim  26151  dvfsumrlim2  26152  fta1g  26288  plyeq0lem  26328  vieta1lem1  26432  vieta1lem2  26433  fsumharmonic  27134  dvdsflf1o  27309  dvdsflsumcom  27310  fsumvma  27335  vmadivsumb  27605  dchrisum0lem1a  27608  dchrisumlema  27610  dchrisumlem3  27613  dchrmusum2  27616  dchrvmasumlem2  27620  dchrvmasumiflem1  27623  dchrisum0fno1  27633  dchrisum0lem1b  27637  mulog2sumlem2  27657  vmalogdivsum2  27660  2vmadivsumlem  27662  selberglem2  27668  selbergb  27671  selberg2b  27674  selberg3lem1  27679  selberg4lem1  27682  pntpbnd1  27708  pntibndlem3  27714  pntlem3  27731  sltsleft  28011  sltsright  28012  cofcutr  28075  oppnid  28977  sspba  30988  sspg  30989  ssps  30991  sspn  30997  nmblore  31047  phpar  31085  ocorth  31552  elnlfn2  32190  foresf1o  32760  fnpreimac  32927  fpwrelmap  32990  elrgspnsubrunlem2  33481  kerunit  33560  0nellinds  33600  linds2eq  33610  dvdsruasso  33614  unitpidl1  33648  mxidlirredi  33671  dflringlem2  33702  rprmdvds  33726  rprmnz  33727  1arithufdlem3  33753  ply1unit  33782  ply1degltlss  33803  selvply1rhmlema  33825  selvply1rhmlem1  33827  esplyfvaln  33881  exsslsb  33904  ply1degltdimlem  33929  lindsunlem  33931  dimkerim  33934  irngss  33994  0ringirng  33996  irngnminplynz  34019  algextdeglem8  34031  reff  34146  cnre2csqlem  34217  fmcncfil  34238  elzrhunit  34284  qqhval2lem  34288  baselsiga  34422  signsply0  34855  cvmliftmolem1  35644  mclsppslem  35946  mclspps  35947  fnetr  36724  relowlssretop  37869  mbfresfi  38177  itg2addnclem  38182  itg2addnclem2  38183  sstotbnd2  38285  rngoiso1o  38490  pridl  38548  lfli  39697  lkrf0  39729  cvrne  39917  atcvr0  39924  psubspi  40383  psubcli2N  40575  lhp1cvr  40635  lautle  40720  diadmleN  41674  sn-eluzp1l  42929  cvgdvgrat  44887  radcnvrat  44888  projf1o  45772  islptre  46193  islpcn  46211  icccncfext  46459  fdivmptf  49172  refdivmptf  49173  rege1logbrege0  49189  nelsubc2  49698  termcterm2  50143