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  9693  fseqenlem2  10105  axdc3lem2  10530  fpwwe2lem11  10727  rlimsqzlem  15817  ramub1lem2  17206  invfun  17940  pltne  18507  cntzi  19544  odmulg  19771  subgslw  19831  frgpnabllem1  20088  cyggeninv  20098  ablfaclem3  20304  lsslmod  21236  rhmpreimaidl  21572  rhmpreimaprmidl  21636  psgnevpm  21896  pjff  22019  pjf2  22021  pjcss  22023  ocvpj  22024  evlslem3  22390  mhpdeg  22467  scmatscmid  22822  fvmptnn04ifc  23171  fvmptnn04ifd  23172  tgcl  23288  cldopn  23350  cncnp  23599  1stcelcls  23781  lly1stc  23816  refssex  23831  qtoptop2  24019  qtopid  24025  trfg  24211  flfneii  24312  fclsbas  24341  isfcf  24354  restutop  24557  restutopopn  24558  isucn2  24598  cfiluexsm  24609  cfilufg  24612  blgt0  24719  xblss2ps  24721  xblss2  24722  mopni  24812  metrest  24844  metustbl  24886  restmetu  24890  cfilss  25592  caun0  25603  cmetcaulem  25610  cfilresi  25617  cmetcusp  25676  cnlimci  26210  dvcl  26220  dvcnp  26240  dvcnp2  26241  dvnadd  26250  dvfsumrlimge0  26351  dvfsumrlim  26352  dvfsumrlim2  26353  fta1g  26489  plyeq0lem  26530  vieta1lem1  26634  vieta1lem2  26635  fsumharmonic  27340  dvdsflf1o  27515  dvdsflsumcom  27516  fsumvma  27541  vmadivsumb  27811  dchrisum0lem1a  27814  dchrisumlema  27816  dchrisumlem3  27819  dchrmusum2  27822  dchrvmasumlem2  27826  dchrvmasumiflem1  27829  dchrisum0fno1  27839  dchrisum0lem1b  27843  mulog2sumlem2  27863  vmalogdivsum2  27866  2vmadivsumlem  27868  selberglem2  27874  selbergb  27877  selberg2b  27880  selberg3lem1  27885  selberg4lem1  27888  pntpbnd1  27914  pntibndlem3  27920  pntlem3  27937  sltsleft  28247  sltsright  28248  cofcutr  28311  oppnid  29223  prlnghpg  29425  sspba  31330  sspg  31331  ssps  31333  sspn  31339  nmblore  31389  phpar  31427  ocorth  31894  elnlfn2  32532  foresf1o  33143  fnpreimac  33307  fpwrelmap  33368  elrgspnsubrunlem2  33852  kerunit  33929  0nellinds  33969  linds2eq  33979  dvdsruasso  33983  unitpidl1  34017  mxidlirredi  34039  dflringlem2  34070  rprmdvds  34094  rprmnz  34095  1arithufdlem3  34121  ply1unit  34150  ply1degltlss  34171  selvply1rhmlema  34193  selvply1rhmlem1  34195  esplyfvaln  34249  exsslsb  34272  ply1degltdimlem  34297  lindsunlem  34299  dimkerim  34302  irngss  34362  0ringirng  34364  irngnminplynz  34387  algextdeglem8  34399  reff  34514  cnre2csqlem  34585  fmcncfil  34606  elzrhunit  34652  qqhval2lem  34656  baselsiga  34790  signsply0  35223  cvmliftmolem1  36115  mclsppslem  36417  mclspps  36418  fnetr  37214  relowlssretop  38362  mbfresfi  38660  itg2addnclem  38665  itg2addnclem2  38666  sstotbnd2  38784  rngoiso1o  38989  pridl  39047  lfli  40194  lkrf0  40226  cvrne  40414  atcvr0  40421  psubspi  40880  psubcli2N  41072  lhp1cvr  41132  lautle  41217  diadmleN  42171  sn-eluzp1l  43441  prjspnnorm  43737  cvgdvgrat  45373  radcnvrat  45374  projf1o  46287  islptre  46707  islpcn  46725  icccncfext  46973  fdivmptf  49729  refdivmptf  49730  rege1logbrege0  49746  nelsubc2  50253  termcterm2  50698