Theorem simplbda 505

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

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

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 402

This theorem is used by:  cantnflem3  9670  fseqenlem2  10076  axdc3lem2  10501  fpwwe2lem11  10698  rlimsqzlem  15784  ramub1lem2  17167  invfun  17901  pltne  18468  cntzi  19505  odmulg  19732  subgslw  19792  frgpnabllem1  20049  cyggeninv  20059  ablfaclem3  20265  lsslmod  21197  rhmpreimaidl  21533  rhmpreimaprmidl  21597  psgnevpm  21857  pjff  21980  pjf2  21982  pjcss  21984  ocvpj  21985  evlslem3  22351  mhpdeg  22428  scmatscmid  22783  fvmptnn04ifc  23132  fvmptnn04ifd  23133  tgcl  23249  cldopn  23311  cncnp  23560  1stcelcls  23742  lly1stc  23777  refssex  23792  qtoptop2  23980  qtopid  23986  trfg  24172  flfneii  24273  fclsbas  24302  isfcf  24315  restutop  24518  restutopopn  24519  isucn2  24559  cfiluexsm  24570  cfilufg  24573  blgt0  24680  xblss2ps  24682  xblss2  24683  mopni  24773  metrest  24805  metustbl  24847  restmetu  24851  cfilss  25553  caun0  25564  cmetcaulem  25571  cfilresi  25578  cmetcusp  25637  cnlimci  26171  dvcl  26181  dvcnp  26201  dvcnp2  26202  dvnadd  26211  dvfsumrlimge0  26312  dvfsumrlim  26313  dvfsumrlim2  26314  fta1g  26450  plyeq0lem  26491  vieta1lem1  26597  vieta1lem2  26598  fsumharmonic  27303  dvdsflf1o  27478  dvdsflsumcom  27479  fsumvma  27504  vmadivsumb  27774  dchrisum0lem1a  27777  dchrisumlema  27779  dchrisumlem3  27782  dchrmusum2  27785  dchrvmasumlem2  27789  dchrvmasumiflem1  27792  dchrisum0fno1  27802  dchrisum0lem1b  27806  mulog2sumlem2  27826  vmalogdivsum2  27829  2vmadivsumlem  27831  selberglem2  27837  selbergb  27840  selberg2b  27843  selberg3lem1  27848  selberg4lem1  27851  pntpbnd1  27877  pntibndlem3  27883  pntlem3  27900  sltsleft  28180  sltsright  28181  cofcutr  28244  oppnid  29156  prlnghpg  29358  sspba  31263  sspg  31264  ssps  31266  sspn  31272  nmblore  31322  phpar  31360  ocorth  31827  elnlfn2  32465  foresf1o  33034  fnpreimac  33198  fpwrelmap  33259  elrgspnsubrunlem2  33743  kerunit  33820  0nellinds  33860  linds2eq  33870  dvdsruasso  33874  unitpidl1  33908  mxidlirredi  33930  dflringlem2  33961  rprmdvds  33985  rprmnz  33986  1arithufdlem3  34012  ply1unit  34041  ply1degltlss  34062  selvply1rhmlema  34084  selvply1rhmlem1  34086  esplyfvaln  34140  exsslsb  34163  ply1degltdimlem  34188  lindsunlem  34190  dimkerim  34193  irngss  34253  0ringirng  34255  irngnminplynz  34278  algextdeglem8  34290  reff  34405  cnre2csqlem  34476  fmcncfil  34497  elzrhunit  34543  qqhval2lem  34547  baselsiga  34681  signsply0  35115  cvmliftmolem1  35967  mclsppslem  36269  mclspps  36270  fnetr  37061  relowlssretop  38206  mbfresfi  38504  itg2addnclem  38509  itg2addnclem2  38510  sstotbnd2  38628  rngoiso1o  38833  pridl  38891  lfli  40038  lkrf0  40070  cvrne  40258  atcvr0  40265  psubspi  40724  psubcli2N  40916  lhp1cvr  40976  lautle  41061  diadmleN  42015  sn-eluzp1l  43287  cvgdvgrat  45241  radcnvrat  45242  projf1o  46132  islptre  46553  islpcn  46571  icccncfext  46819  fdivmptf  49575  refdivmptf  49576  rege1logbrege0  49592  nelsubc2  50099  termcterm2  50544