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  9728  fseqenlem2  10062  axdc3lem2  10488  fpwwe2lem11  10678  rlimsqzlem  15681  ramub1lem2  17060  invfun  17811  pltne  18391  cntzi  19359  odmulg  19588  subgslw  19648  frgpnabllem1  19905  cyggeninv  19915  ablfaclem3  20121  lsslmod  20975  rhmpreimaidl  21304  psgnevpm  21624  pjff  21749  pjf2  21751  pjcss  21753  ocvpj  21754  evlslem3  22121  mhpdeg  22166  scmatscmid  22527  fvmptnn04ifc  22873  fvmptnn04ifd  22874  tgcl  22991  cldopn  23054  cncnp  23303  1stcelcls  23484  lly1stc  23519  refssex  23534  qtoptop2  23722  qtopid  23728  trfg  23914  flfneii  24015  fclsbas  24044  isfcf  24057  restutop  24261  restutopopn  24262  isucn2  24303  cfiluexsm  24314  cfilufg  24317  blgt0  24424  xblss2ps  24426  xblss2  24427  mopni  24520  metrest  24552  metustbl  24594  restmetu  24598  cfilss  25317  caun0  25328  cmetcaulem  25335  cfilresi  25342  cmetcusp  25401  cnlimci  25938  dvcl  25948  dvcnp  25968  dvcnp2  25969  dvcnp2OLD  25970  dvnadd  25979  dvfsumrlimge0  26085  dvfsumrlim  26086  dvfsumrlim2  26087  fta1g  26223  plyeq0lem  26263  vieta1lem1  26366  vieta1lem2  26367  fsumharmonic  27069  dvdsflf1o  27244  dvdsflsumcom  27245  fsumvma  27271  vmadivsumb  27541  dchrisum0lem1a  27544  dchrisumlema  27546  dchrisumlem3  27549  dchrmusum2  27552  dchrvmasumlem2  27556  dchrvmasumiflem1  27559  dchrisum0fno1  27569  dchrisum0lem1b  27573  mulog2sumlem2  27593  vmalogdivsum2  27596  2vmadivsumlem  27598  selberglem2  27604  selbergb  27607  selberg2b  27610  selberg3lem1  27615  selberg4lem1  27618  pntpbnd1  27644  pntibndlem3  27650  pntlem3  27667  ssltleft  27923  ssltright  27924  cofcutr  27972  oppnid  28768  sspba  30755  sspg  30756  ssps  30758  sspn  30764  nmblore  30814  phpar  30852  ocorth  31319  elnlfn2  31957  foresf1o  32531  fnpreimac  32687  fpwrelmap  32750  kerunit  33328  0nellinds  33377  linds2eq  33388  dvdsruasso  33392  unitpidl1  33431  rhmpreimaprmidl  33458  mxidlirredi  33478  rprmdvds  33526  rprmnz  33527  1arithufdlem3  33553  ply1unit  33579  ply1degltlss  33596  ply1degltdimlem  33649  lindsunlem  33651  dimkerim  33654  irngss  33701  0ringirng  33703  irngnminplynz  33719  algextdeglem8  33729  reff  33799  cnre2csqlem  33870  fmcncfil  33891  elzrhunit  33939  qqhval2lem  33943  baselsiga  34095  signsply0  34544  cvmliftmolem1  35265  mclsppslem  35567  mclspps  35568  fnetr  36333  relowlssretop  37345  mbfresfi  37652  itg2addnclem  37657  itg2addnclem2  37658  sstotbnd2  37760  rngoiso1o  37965  pridl  38023  lfli  39042  lkrf0  39074  cvrne  39262  atcvr0  39269  psubspi  39729  psubcli2N  39921  lhp1cvr  39981  lautle  40066  diadmleN  41020  sn-eluzp1l  42320  cvgdvgrat  44308  radcnvrat  44309  projf1o  45139  islptre  45574  islpcn  45594  icccncfext  45842  fdivmptf  48390  refdivmptf  48391  rege1logbrege0  48407