Theorem simprbda 503

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

Hypothesis

Ref	Expression
simplbda.1	⊢ (𝜑 → (𝜓 ↔ (𝜒 ∧ 𝜃)))

Assertion

Ref	Expression
simprbda	⊢ ((𝜑 ∧ 𝜓) → 𝜒)

Proof of Theorem simprbda

Step	Hyp	Ref	Expression
1		simplbda.1	. . 3 ⊢ (𝜑 → (𝜓 ↔ (𝜒 ∧ 𝜃)))
2	1	biimpa 481	. 2 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 ∧ 𝜃))
3	2	simpld 499	1 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  oteqex  5484  fsnex  7282  fisupg  9247  fiinfg  9460  cantnff  9642  fseqenlem2  10008  fpwwe2lem10  10624  fpwwe2lem11  10625  fpwwe2  10627  rlimsqzlem  15699  ramub1lem2  17086  mriss  17690  invfun  17820  pltle  18386  subgslw  19685  frgpnabllem2  19943  cyggeninv  19952  ablfaclem3  20158  lmodfopnelem1  20996  ssdifidllem  21452  pjff  21830  pjf2  21832  pjfo  21833  pjcss  21834  mplind  22189  mhpmpl  22275  fvmptnn04ifc  22977  chfacfisf  22979  chfacfisfcpmat  22980  tg1  23089  cldss  23154  cnf2  23374  cncnp  23405  lly1stc  23621  refbas  23635  qtoptop2  23824  qtoprest  23842  elfm3  24075  flfelbas  24119  cnextf  24191  restutopopn  24363  cfilufbas  24413  fmucnd  24416  blgt0  24524  xblss2ps  24526  xblss2  24527  tngngp  24779  cfilfil  25394  iscau2  25404  caufpm  25409  cmetcaulem  25415  dvcnp2  26047  dvfsumrlim  26158  dvfsumrlim2  26159  fta1g  26295  dvdsflsumcom  27317  fsumvma  27342  vmadivsumb  27612  dchrisumlema  27617  dchrvmasumlem1  27624  dchrvmasum2lem  27625  dchrvmasumiflem1  27630  selbergb  27678  selberg2b  27681  pntibndlem3  27721  pntlem3  27738  motgrp  28777  oppnid  28985  sspnv  31018  lnof  31047  bloln  31076  dfmgc2  33256  elrgspnsubrunlem2  33508  dflringlem2  33729  rprmcl  33752  rprmnz  33754  rprmnunit  33755  ply1unit  33809  fldexttr  33992  algextdeglem8  34058  reff  34173  signsply0  34882  cvmliftmolem1  35671  cvmlift2lem9a  35693  mbfresfi  38204  itg2gt0cn  38213  ismtyres  38346  ghomf  38428  rngoisohom  38518  pridlidl  38573  pridlnr  38574  maxidlidl  38579  lflf  39726  lkrcl  39755  cvrlt  39933  cvrle  39941  atbase  39952  llnbase  40172  lplnbase  40197  lvolbase  40241  psubssat  40417  lhpbase  40661  laut1o  40748  ldillaut  40774  ltrnldil  40785  diadmclN  41700  pell1234qrre  43470  lnmlsslnm  43699  cantnf2  43943  naddcnfid1  43985  cvgdvgrat  44914  stoweidlem34  46639  mpbiran3d  49459