Theorem simprbda 499

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 477	. 2 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 ∧ 𝜃))
3	2	simpld 495	1 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)

Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  oteqex  5448  fsnex  7234  fisupg  9195  fiinfg  9411  cantnff  9593  fseqenlem2  9945  fpwwe2lem10  10561  fpwwe2lem11  10562  fpwwe2  10564  rlimsqzlem  15609  ramub1lem2  16996  mriss  17599  invfun  17729  pltle  18295  subgslw  19589  frgpnabllem2  19847  cyggeninv  19856  ablfaclem3  20062  lmodfopnelem1  20895  pjff  21694  pjf2  21696  pjfo  21697  pjcss  21698  mplind  22053  mhpmpl  22139  fvmptnn04ifc  22842  chfacfisf  22844  chfacfisfcpmat  22845  tg1  22954  cldss  23019  cnf2  23239  cncnp  23270  lly1stc  23486  refbas  23500  qtoptop2  23689  qtoprest  23707  elfm3  23940  flfelbas  23984  cnextf  24056  restutopopn  24228  cfilufbas  24278  fmucnd  24281  blgt0  24389  xblss2ps  24391  xblss2  24392  tngngp  24644  cfilfil  25259  iscau2  25269  caufpm  25274  cmetcaulem  25280  dvcnp2  25912  dvfsumrlim  26023  dvfsumrlim2  26024  fta1g  26160  dvdsflsumcom  27176  fsumvma  27201  vmadivsumb  27471  dchrisumlema  27476  dchrvmasumlem1  27483  dchrvmasum2lem  27484  dchrvmasumiflem1  27489  selbergb  27537  selberg2b  27540  pntibndlem3  27580  pntlem3  27597  motgrp  28636  oppnid  28839  sspnv  30822  lnof  30851  bloln  30880  dfmgc2  33082  elrgspnsubrunlem2  33336  ssdifidllem  33546  rprmcl  33608  rprmnz  33610  rprmnunit  33611  ply1unit  33665  fldexttr  33849  algextdeglem8  33915  reff  34030  signsply0  34742  cvmliftmolem1  35510  cvmlift2lem9a  35532  mbfresfi  38034  itg2gt0cn  38043  ismtyres  38176  ghomf  38258  rngoisohom  38348  pridlidl  38403  pridlnr  38404  maxidlidl  38409  lflf  39556  lkrcl  39585  cvrlt  39763  cvrle  39771  atbase  39782  llnbase  40002  lplnbase  40027  lvolbase  40071  psubssat  40247  lhpbase  40491  laut1o  40578  ldillaut  40604  ltrnldil  40615  diadmclN  41530  pell1234qrre  43298  lnmlsslnm  43527  cantnf2  43771  naddcnfid1  43813  cvgdvgrat  44758  stoweidlem34  46478  mpbiran3d  49288