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  9731  fseqenlem2  10065  axdc3lem2  10491  fpwwe2lem11  10681  rlimsqzlem  15685  ramub1lem2  17065  invfun  17808  pltne  18379  cntzi  19347  odmulg  19574  subgslw  19634  frgpnabllem1  19891  cyggeninv  19901  ablfaclem3  20107  lsslmod  20958  rhmpreimaidl  21287  psgnevpm  21607  pjff  21732  pjf2  21734  pjcss  21736  ocvpj  21737  evlslem3  22104  mhpdeg  22149  scmatscmid  22512  fvmptnn04ifc  22858  fvmptnn04ifd  22859  tgcl  22976  cldopn  23039  cncnp  23288  1stcelcls  23469  lly1stc  23504  refssex  23519  qtoptop2  23707  qtopid  23713  trfg  23899  flfneii  24000  fclsbas  24029  isfcf  24042  restutop  24246  restutopopn  24247  isucn2  24288  cfiluexsm  24299  cfilufg  24302  blgt0  24409  xblss2ps  24411  xblss2  24412  mopni  24505  metrest  24537  metustbl  24579  restmetu  24583  cfilss  25304  caun0  25315  cmetcaulem  25322  cfilresi  25329  cmetcusp  25388  cnlimci  25924  dvcl  25934  dvcnp  25954  dvcnp2  25955  dvcnp2OLD  25956  dvnadd  25965  dvfsumrlimge0  26071  dvfsumrlim  26072  dvfsumrlim2  26073  fta1g  26209  plyeq0lem  26249  vieta1lem1  26352  vieta1lem2  26353  fsumharmonic  27055  dvdsflf1o  27230  dvdsflsumcom  27231  fsumvma  27257  vmadivsumb  27527  dchrisum0lem1a  27530  dchrisumlema  27532  dchrisumlem3  27535  dchrmusum2  27538  dchrvmasumlem2  27542  dchrvmasumiflem1  27545  dchrisum0fno1  27555  dchrisum0lem1b  27559  mulog2sumlem2  27579  vmalogdivsum2  27582  2vmadivsumlem  27584  selberglem2  27590  selbergb  27593  selberg2b  27596  selberg3lem1  27601  selberg4lem1  27604  pntpbnd1  27630  pntibndlem3  27636  pntlem3  27653  ssltleft  27909  ssltright  27910  cofcutr  27958  oppnid  28754  sspba  30746  sspg  30747  ssps  30749  sspn  30755  nmblore  30805  phpar  30843  ocorth  31310  elnlfn2  31948  foresf1o  32523  fnpreimac  32681  fpwrelmap  32744  elrgspnsubrunlem2  33252  kerunit  33349  0nellinds  33398  linds2eq  33409  dvdsruasso  33413  unitpidl1  33452  rhmpreimaprmidl  33479  mxidlirredi  33499  rprmdvds  33547  rprmnz  33548  1arithufdlem3  33574  ply1unit  33600  ply1degltlss  33617  exsslsb  33647  ply1degltdimlem  33673  lindsunlem  33675  dimkerim  33678  irngss  33737  0ringirng  33739  irngnminplynz  33755  algextdeglem8  33765  reff  33838  cnre2csqlem  33909  fmcncfil  33930  elzrhunit  33978  qqhval2lem  33982  baselsiga  34116  signsply0  34566  cvmliftmolem1  35286  mclsppslem  35588  mclspps  35589  fnetr  36352  relowlssretop  37364  mbfresfi  37673  itg2addnclem  37678  itg2addnclem2  37679  sstotbnd2  37781  rngoiso1o  37986  pridl  38044  lfli  39062  lkrf0  39094  cvrne  39282  atcvr0  39289  psubspi  39749  psubcli2N  39941  lhp1cvr  40001  lautle  40086  diadmleN  41040  sn-eluzp1l  42342  cvgdvgrat  44332  radcnvrat  44333  projf1o  45202  islptre  45634  islpcn  45654  icccncfext  45902  fdivmptf  48462  refdivmptf  48463  rege1logbrege0  48479  termcterm2  49146