Theorem simprbda 499

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

Hypothesis

Ref	Expression
pm3.26bda.1	⊢ (𝜑 → (𝜓 ↔ (𝜒 ∧ 𝜃)))

Assertion

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

Proof of Theorem simprbda

Step	Hyp	Ref	Expression
1		pm3.26bda.1	. . 3 ⊢ (𝜑 → (𝜓 ↔ (𝜒 ∧ 𝜃)))
2	1	biimpa 477	. 2 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 ∧ 𝜃))
3	2	simpld 495	1 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)

Syntax hints:   → wi 4   ↔ wb 205   ∧ 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 206  df-an 397

This theorem is referenced by:  elrabiOLD  3620  oteqex  5415  fsnex  7164  fisupg  9071  fiinfg  9267  cantnff  9441  fseqenlem2  9790  fpwwe2lem10  10405  fpwwe2lem11  10406  fpwwe2  10408  rlimsqzlem  15369  ramub1lem2  16737  mriss  17353  invfun  17485  pltle  18060  subgslw  19230  frgpnabllem2  19484  cyggeninv  19492  ablfaclem3  19699  lmodfopnelem1  20168  pjff  20928  pjf2  20930  pjfo  20931  pjcss  20932  psrbagfOLD  21131  mplind  21287  mhpmpl  21343  fvmptnn04ifc  22010  chfacfisf  22012  chfacfisfcpmat  22013  tg1  22123  cldss  22189  cnf2  22409  cncnp  22440  lly1stc  22656  refbas  22670  qtoptop2  22859  qtoprest  22877  elfm3  23110  flfelbas  23154  cnextf  23226  restutopopn  23399  cfilufbas  23450  fmucnd  23453  blgt0  23561  xblss2ps  23563  xblss2  23564  tngngp  23827  cfilfil  24440  iscau2  24450  caufpm  24455  cmetcaulem  24461  dvcnp2  25093  dvfsumrlim  25204  dvfsumrlim2  25205  fta1g  25341  dvdsflsumcom  26346  fsumvma  26370  vmadivsumb  26640  dchrisumlema  26645  dchrvmasumlem1  26652  dchrvmasum2lem  26653  dchrvmasumiflem1  26658  selbergb  26706  selberg2b  26709  pntibndlem3  26749  pntlem3  26766  motgrp  26913  oppnid  27116  sspnv  29097  lnof  29126  bloln  29155  dfmgc2  31283  fldexttr  31742  reff  31798  signsply0  32539  cvmliftmolem1  33252  cvmlift2lem9a  33274  mbfresfi  35832  itg2gt0cn  35841  ismtyres  35975  ghomf  36057  rngoisohom  36147  pridlidl  36202  pridlnr  36203  maxidlidl  36208  lflf  37084  lkrcl  37113  cvrlt  37291  cvrle  37299  atbase  37310  llnbase  37530  lplnbase  37555  lvolbase  37599  psubssat  37775  lhpbase  38019  laut1o  38106  ldillaut  38132  ltrnldil  38143  diadmclN  39058  pell1234qrre  40681  lnmlsslnm  40913  cvgdvgrat  41938  stoweidlem34  43582  mpbiran3d  46153