Theorem simplbda 499

Description: Deduction eliminating a conjunct. (Contributed by NM, 22-Oct-2007.)

Hypothesis

Ref	Expression
pm3.26bda.1	⊢ (𝜑 → (𝜓 ↔ (𝜒 ∧ 𝜃)))

Assertion

Ref	Expression
simplbda	⊢ ((𝜑 ∧ 𝜓) → 𝜃)

Proof of Theorem simplbda

Step	Hyp	Ref	Expression
1		pm3.26bda.1	. . 3 ⊢ (𝜑 → (𝜓 ↔ (𝜒 ∧ 𝜃)))
2	1	biimpa 476	. 2 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 ∧ 𝜃))
3	2	simprd 495	1 ⊢ ((𝜑 ∧ 𝜓) → 𝜃)

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  cantnflem3  9604  fseqenlem2  9939  axdc3lem2  10365  fpwwe2lem11  10556  rlimsqzlem  15576  ramub1lem2  16959  invfun  17692  pltne  18259  cntzi  19262  odmulg  19489  subgslw  19549  frgpnabllem1  19806  cyggeninv  19816  ablfaclem3  20022  lsslmod  20915  rhmpreimaidl  21236  psgnevpm  21548  pjff  21671  pjf2  21673  pjcss  21675  ocvpj  21676  evlslem3  22039  mhpdeg  22092  scmatscmid  22454  fvmptnn04ifc  22800  fvmptnn04ifd  22801  tgcl  22917  cldopn  22979  cncnp  23228  1stcelcls  23409  lly1stc  23444  refssex  23459  qtoptop2  23647  qtopid  23653  trfg  23839  flfneii  23940  fclsbas  23969  isfcf  23982  restutop  24185  restutopopn  24186  isucn2  24226  cfiluexsm  24237  cfilufg  24240  blgt0  24347  xblss2ps  24349  xblss2  24350  mopni  24440  metrest  24472  metustbl  24514  restmetu  24518  cfilss  25230  caun0  25241  cmetcaulem  25248  cfilresi  25255  cmetcusp  25314  cnlimci  25850  dvcl  25860  dvcnp  25880  dvcnp2  25881  dvcnp2OLD  25882  dvnadd  25891  dvfsumrlimge0  25997  dvfsumrlim  25998  dvfsumrlim2  25999  fta1g  26135  plyeq0lem  26175  vieta1lem1  26278  vieta1lem2  26279  fsumharmonic  26982  dvdsflf1o  27157  dvdsflsumcom  27158  fsumvma  27184  vmadivsumb  27454  dchrisum0lem1a  27457  dchrisumlema  27459  dchrisumlem3  27462  dchrmusum2  27465  dchrvmasumlem2  27469  dchrvmasumiflem1  27472  dchrisum0fno1  27482  dchrisum0lem1b  27486  mulog2sumlem2  27506  vmalogdivsum2  27509  2vmadivsumlem  27511  selberglem2  27517  selbergb  27520  selberg2b  27523  selberg3lem1  27528  selberg4lem1  27531  pntpbnd1  27557  pntibndlem3  27563  pntlem3  27580  ssltleft  27852  ssltright  27853  cofcutr  27906  oppnid  28801  sspba  30785  sspg  30786  ssps  30788  sspn  30794  nmblore  30844  phpar  30882  ocorth  31349  elnlfn2  31987  foresf1o  32561  fnpreimac  32730  fpwrelmap  32793  elrgspnsubrunlem2  33311  kerunit  33387  0nellinds  33432  linds2eq  33443  dvdsruasso  33447  unitpidl1  33486  rhmpreimaprmidl  33513  mxidlirredi  33533  rprmdvds  33581  rprmnz  33582  1arithufdlem3  33608  ply1unit  33637  ply1degltlss  33658  exsslsb  33734  ply1degltdimlem  33760  lindsunlem  33762  dimkerim  33765  irngss  33825  0ringirng  33827  irngnminplynz  33850  algextdeglem8  33862  reff  33977  cnre2csqlem  34048  fmcncfil  34069  elzrhunit  34115  qqhval2lem  34119  baselsiga  34253  signsply0  34689  cvmliftmolem1  35456  mclsppslem  35758  mclspps  35759  fnetr  36526  relowlssretop  37539  mbfresfi  37838  itg2addnclem  37843  itg2addnclem2  37844  sstotbnd2  37946  rngoiso1o  38151  pridl  38209  lfli  39358  lkrf0  39390  cvrne  39578  atcvr0  39585  psubspi  40044  psubcli2N  40236  lhp1cvr  40296  lautle  40381  diadmleN  41335  sn-eluzp1l  42599  cvgdvgrat  44590  radcnvrat  44591  projf1o  45477  islptre  45901  islpcn  45919  icccncfext  46167  fdivmptf  48823  refdivmptf  48824  rege1logbrege0  48840  nelsubc2  49350  termcterm2  49795