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  9673  fseqenlem2  10031  axdc3lem2  10456  fpwwe2lem11  10653  rlimsqzlem  15738  ramub1lem2  17123  invfun  17857  pltne  18424  cntzi  19457  odmulg  19684  subgslw  19744  frgpnabllem1  20001  cyggeninv  20011  ablfaclem3  20217  lsslmod  21145  rhmpreimaidl  21480  rhmpreimaprmidl  21543  psgnevpm  21803  pjff  21926  pjf2  21928  pjcss  21930  ocvpj  21931  evlslem3  22297  mhpdeg  22374  scmatscmid  22729  fvmptnn04ifc  23078  fvmptnn04ifd  23079  tgcl  23195  cldopn  23257  cncnp  23506  1stcelcls  23688  lly1stc  23723  refssex  23738  qtoptop2  23926  qtopid  23932  trfg  24118  flfneii  24219  fclsbas  24248  isfcf  24261  restutop  24464  restutopopn  24465  isucn2  24505  cfiluexsm  24516  cfilufg  24519  blgt0  24626  xblss2ps  24628  xblss2  24629  mopni  24719  metrest  24751  metustbl  24793  restmetu  24797  cfilss  25499  caun0  25510  cmetcaulem  25517  cfilresi  25524  cmetcusp  25583  cnlimci  26118  dvcl  26128  dvcnp  26148  dvcnp2  26149  dvnadd  26158  dvfsumrlimge0  26259  dvfsumrlim  26260  dvfsumrlim2  26261  fta1g  26397  plyeq0lem  26437  vieta1lem1  26541  vieta1lem2  26542  fsumharmonic  27246  dvdsflf1o  27421  dvdsflsumcom  27422  fsumvma  27447  vmadivsumb  27717  dchrisum0lem1a  27720  dchrisumlema  27722  dchrisumlem3  27725  dchrmusum2  27728  dchrvmasumlem2  27732  dchrvmasumiflem1  27735  dchrisum0fno1  27745  dchrisum0lem1b  27749  mulog2sumlem2  27769  vmalogdivsum2  27772  2vmadivsumlem  27774  selberglem2  27780  selbergb  27783  selberg2b  27786  selberg3lem1  27791  selberg4lem1  27794  pntpbnd1  27820  pntibndlem3  27826  pntlem3  27843  sltsleft  28123  sltsright  28124  cofcutr  28187  oppnid  29099  prlnghpg  29289  sspba  31194  sspg  31195  ssps  31197  sspn  31203  nmblore  31253  phpar  31291  ocorth  31758  elnlfn2  32396  foresf1o  32965  fnpreimac  33130  fpwrelmap  33191  elrgspnsubrunlem2  33675  kerunit  33752  0nellinds  33792  linds2eq  33801  dvdsruasso  33805  unitpidl1  33839  mxidlirredi  33861  dflringlem2  33892  rprmdvds  33916  rprmnz  33917  1arithufdlem3  33943  ply1unit  33972  ply1degltlss  33993  selvply1rhmlema  34015  selvply1rhmlem1  34017  esplyfvaln  34071  exsslsb  34094  ply1degltdimlem  34119  lindsunlem  34121  dimkerim  34124  irngss  34184  0ringirng  34186  irngnminplynz  34209  algextdeglem8  34221  reff  34336  cnre2csqlem  34407  fmcncfil  34428  elzrhunit  34474  qqhval2lem  34478  baselsiga  34612  signsply0  35046  cvmliftmolem1  35847  mclsppslem  36149  mclspps  36150  fnetr  36957  relowlssretop  38104  mbfresfi  38402  itg2addnclem  38407  itg2addnclem2  38408  sstotbnd2  38511  rngoiso1o  38716  pridl  38774  lfli  39921  lkrf0  39953  cvrne  40141  atcvr0  40148  psubspi  40607  psubcli2N  40799  lhp1cvr  40859  lautle  40944  diadmleN  41898  sn-eluzp1l  43170  cvgdvgrat  45124  radcnvrat  45125  projf1o  46015  islptre  46436  islpcn  46454  icccncfext  46702  fdivmptf  49458  refdivmptf  49459  rege1logbrege0  49475  nelsubc2  49982  termcterm2  50427