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  9606  fseqenlem2  9938  axdc3lem2  10364  fpwwe2lem11  10554  rlimsqzlem  15574  ramub1lem2  16957  invfun  17689  pltne  18256  cntzi  19226  odmulg  19453  subgslw  19513  frgpnabllem1  19770  cyggeninv  19780  ablfaclem3  19986  lsslmod  20881  rhmpreimaidl  21202  psgnevpm  21514  pjff  21637  pjf2  21639  pjcss  21641  ocvpj  21642  evlslem3  22003  mhpdeg  22048  scmatscmid  22409  fvmptnn04ifc  22755  fvmptnn04ifd  22756  tgcl  22872  cldopn  22934  cncnp  23183  1stcelcls  23364  lly1stc  23399  refssex  23414  qtoptop2  23602  qtopid  23608  trfg  23794  flfneii  23895  fclsbas  23924  isfcf  23937  restutop  24141  restutopopn  24142  isucn2  24182  cfiluexsm  24193  cfilufg  24196  blgt0  24303  xblss2ps  24305  xblss2  24306  mopni  24396  metrest  24428  metustbl  24470  restmetu  24474  cfilss  25186  caun0  25197  cmetcaulem  25204  cfilresi  25211  cmetcusp  25270  cnlimci  25806  dvcl  25816  dvcnp  25836  dvcnp2  25837  dvcnp2OLD  25838  dvnadd  25847  dvfsumrlimge0  25953  dvfsumrlim  25954  dvfsumrlim2  25955  fta1g  26091  plyeq0lem  26131  vieta1lem1  26234  vieta1lem2  26235  fsumharmonic  26938  dvdsflf1o  27113  dvdsflsumcom  27114  fsumvma  27140  vmadivsumb  27410  dchrisum0lem1a  27413  dchrisumlema  27415  dchrisumlem3  27418  dchrmusum2  27421  dchrvmasumlem2  27425  dchrvmasumiflem1  27428  dchrisum0fno1  27438  dchrisum0lem1b  27442  mulog2sumlem2  27462  vmalogdivsum2  27465  2vmadivsumlem  27467  selberglem2  27473  selbergb  27476  selberg2b  27479  selberg3lem1  27484  selberg4lem1  27487  pntpbnd1  27513  pntibndlem3  27519  pntlem3  27536  ssltleft  27802  ssltright  27803  cofcutr  27855  oppnid  28709  sspba  30689  sspg  30690  ssps  30692  sspn  30698  nmblore  30748  phpar  30786  ocorth  31253  elnlfn2  31891  foresf1o  32466  fnpreimac  32628  fpwrelmap  32689  elrgspnsubrunlem2  33198  kerunit  33273  0nellinds  33317  linds2eq  33328  dvdsruasso  33332  unitpidl1  33371  rhmpreimaprmidl  33398  mxidlirredi  33418  rprmdvds  33466  rprmnz  33467  1arithufdlem3  33493  ply1unit  33520  ply1degltlss  33538  exsslsb  33568  ply1degltdimlem  33594  lindsunlem  33596  dimkerim  33599  irngss  33658  0ringirng  33660  irngnminplynz  33678  algextdeglem8  33690  reff  33805  cnre2csqlem  33876  fmcncfil  33897  elzrhunit  33943  qqhval2lem  33947  baselsiga  34081  signsply0  34518  cvmliftmolem1  35253  mclsppslem  35555  mclspps  35556  fnetr  36324  relowlssretop  37336  mbfresfi  37645  itg2addnclem  37650  itg2addnclem2  37651  sstotbnd2  37753  rngoiso1o  37958  pridl  38016  lfli  39039  lkrf0  39071  cvrne  39259  atcvr0  39266  psubspi  39726  psubcli2N  39918  lhp1cvr  39978  lautle  40063  diadmleN  41017  sn-eluzp1l  42281  cvgdvgrat  44286  radcnvrat  44287  projf1o  45175  islptre  45601  islpcn  45621  icccncfext  45869  fdivmptf  48514  refdivmptf  48515  rege1logbrege0  48531  nelsubc2  49042  termcterm2  49487