Theorem simplbda 502

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 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  9636  fseqenlem2  9971  axdc3lem2  10398  fpwwe2lem11  10589  rlimsqzlem  15652  ramub1lem2  17039  invfun  17773  pltne  18340  cntzi  19345  odmulg  19572  subgslw  19632  frgpnabllem1  19889  cyggeninv  19899  ablfaclem3  20105  lsslmod  21000  rhmpreimaidl  21320  psgnevpm  21614  pjff  21737  pjf2  21739  pjcss  21741  ocvpj  21742  evlslem3  22106  mhpdeg  22183  scmatscmid  22539  fvmptnn04ifc  22885  fvmptnn04ifd  22886  tgcl  23002  cldopn  23064  cncnp  23313  1stcelcls  23494  lly1stc  23529  refssex  23544  qtoptop2  23732  qtopid  23738  trfg  23924  flfneii  24025  fclsbas  24054  isfcf  24067  restutop  24270  restutopopn  24271  isucn2  24311  cfiluexsm  24322  cfilufg  24325  blgt0  24432  xblss2ps  24434  xblss2  24435  mopni  24525  metrest  24557  metustbl  24599  restmetu  24603  cfilss  25305  caun0  25316  cmetcaulem  25323  cfilresi  25330  cmetcusp  25389  cnlimci  25924  dvcl  25934  dvcnp  25954  dvcnp2  25955  dvnadd  25964  dvfsumrlimge0  26065  dvfsumrlim  26066  dvfsumrlim2  26067  fta1g  26203  plyeq0lem  26243  vieta1lem1  26344  vieta1lem2  26345  fsumharmonic  27046  dvdsflf1o  27221  dvdsflsumcom  27222  fsumvma  27247  vmadivsumb  27517  dchrisum0lem1a  27520  dchrisumlema  27522  dchrisumlem3  27525  dchrmusum2  27528  dchrvmasumlem2  27532  dchrvmasumiflem1  27535  dchrisum0fno1  27545  dchrisum0lem1b  27549  mulog2sumlem2  27569  vmalogdivsum2  27572  2vmadivsumlem  27574  selberglem2  27580  selbergb  27583  selberg2b  27586  selberg3lem1  27591  selberg4lem1  27594  pntpbnd1  27620  pntibndlem3  27626  pntlem3  27643  sltsleft  27923  sltsright  27924  cofcutr  27987  oppnid  28885  sspba  30869  sspg  30870  ssps  30872  sspn  30878  nmblore  30928  phpar  30966  ocorth  31433  elnlfn2  32071  foresf1o  32645  fnpreimac  32815  fpwrelmap  32878  elrgspnsubrunlem2  33383  kerunit  33465  0nellinds  33510  linds2eq  33521  dvdsruasso  33525  unitpidl1  33564  rhmpreimaprmidl  33592  mxidlirredi  33613  dflringlem2  33645  rprmdvds  33669  rprmnz  33670  1arithufdlem3  33696  ply1unit  33725  ply1degltlss  33746  selvply1rhmlema  33769  selvply1rhmlem1  33771  esplyfvaln  33825  exsslsb  33848  ply1degltdimlem  33873  lindsunlem  33875  dimkerim  33878  irngss  33938  0ringirng  33940  irngnminplynz  33963  algextdeglem8  33975  reff  34090  cnre2csqlem  34161  fmcncfil  34182  elzrhunit  34228  qqhval2lem  34232  baselsiga  34366  signsply0  34802  cvmliftmolem1  35579  mclsppslem  35881  mclspps  35882  fnetr  36659  relowlssretop  37805  mbfresfi  38113  itg2addnclem  38118  itg2addnclem2  38119  sstotbnd2  38221  rngoiso1o  38426  pridl  38484  lfli  39633  lkrf0  39665  cvrne  39853  atcvr0  39860  psubspi  40319  psubcli2N  40511  lhp1cvr  40571  lautle  40656  diadmleN  41610  sn-eluzp1l  42865  cvgdvgrat  44837  radcnvrat  44838  projf1o  45722  islptre  46143  islpcn  46161  icccncfext  46409  fdivmptf  49111  refdivmptf  49112  rege1logbrege0  49128  nelsubc2  49638  termcterm2  50083