Theorem simprbda 498

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 476	. 2 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 ∧ 𝜃))
3	2	simpld 494	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:  oteqex  5438  fsnex  7212  fisupg  9167  fiinfg  9380  cantnff  9559  fseqenlem2  9908  fpwwe2lem10  10523  fpwwe2lem11  10524  fpwwe2  10526  rlimsqzlem  15548  ramub1lem2  16931  mriss  17533  invfun  17663  pltle  18229  subgslw  19521  frgpnabllem2  19779  cyggeninv  19788  ablfaclem3  19994  lmodfopnelem1  20824  pjff  21642  pjf2  21644  pjfo  21645  pjcss  21646  mplind  21998  mhpmpl  22052  fvmptnn04ifc  22760  chfacfisf  22762  chfacfisfcpmat  22763  tg1  22872  cldss  22937  cnf2  23157  cncnp  23188  lly1stc  23404  refbas  23418  qtoptop2  23607  qtoprest  23625  elfm3  23858  flfelbas  23902  cnextf  23974  restutopopn  24146  cfilufbas  24196  fmucnd  24199  blgt0  24307  xblss2ps  24309  xblss2  24310  tngngp  24562  cfilfil  25187  iscau2  25197  caufpm  25202  cmetcaulem  25208  dvcnp2  25841  dvcnp2OLD  25842  dvfsumrlim  25958  dvfsumrlim2  25959  fta1g  26095  dvdsflsumcom  27118  fsumvma  27144  vmadivsumb  27414  dchrisumlema  27419  dchrvmasumlem1  27426  dchrvmasum2lem  27427  dchrvmasumiflem1  27432  selbergb  27480  selberg2b  27483  pntibndlem3  27523  pntlem3  27540  motgrp  28514  oppnid  28717  sspnv  30696  lnof  30725  bloln  30754  dfmgc2  32967  elrgspnsubrunlem2  33205  ssdifidllem  33411  rprmcl  33473  rprmnz  33475  rprmnunit  33476  ply1unit  33528  fldexttr  33661  algextdeglem8  33727  reff  33842  signsply0  34554  cvmliftmolem1  35293  cvmlift2lem9a  35315  mbfresfi  37685  itg2gt0cn  37694  ismtyres  37827  ghomf  37909  rngoisohom  37999  pridlidl  38054  pridlnr  38055  maxidlidl  38060  lflf  39081  lkrcl  39110  cvrlt  39288  cvrle  39296  atbase  39307  llnbase  39527  lplnbase  39552  lvolbase  39596  psubssat  39772  lhpbase  40016  laut1o  40103  ldillaut  40129  ltrnldil  40140  diadmclN  41055  pell1234qrre  42864  lnmlsslnm  43093  cantnf2  43337  naddcnfid1  43379  cvgdvgrat  44325  stoweidlem34  46051  mpbiran3d  48807