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  3677  oteqex  5499  fsnex  7277  fisupg  9287  fiinfg  9490  cantnff  9665  fseqenlem2  10016  fpwwe2lem10  10631  fpwwe2lem11  10632  fpwwe2  10634  rlimsqzlem  15591  ramub1lem2  16956  mriss  17575  invfun  17707  pltle  18282  subgslw  19478  frgpnabllem2  19736  cyggeninv  19745  ablfaclem3  19951  lmodfopnelem1  20500  pjff  21258  pjf2  21260  pjfo  21261  pjcss  21262  psrbagfOLD  21463  mplind  21622  mhpmpl  21678  fvmptnn04ifc  22345  chfacfisf  22347  chfacfisfcpmat  22348  tg1  22458  cldss  22524  cnf2  22744  cncnp  22775  lly1stc  22991  refbas  23005  qtoptop2  23194  qtoprest  23212  elfm3  23445  flfelbas  23489  cnextf  23561  restutopopn  23734  cfilufbas  23785  fmucnd  23788  blgt0  23896  xblss2ps  23898  xblss2  23899  tngngp  24162  cfilfil  24775  iscau2  24785  caufpm  24790  cmetcaulem  24796  dvcnp2  25428  dvfsumrlim  25539  dvfsumrlim2  25540  fta1g  25676  dvdsflsumcom  26681  fsumvma  26705  vmadivsumb  26975  dchrisumlema  26980  dchrvmasumlem1  26987  dchrvmasum2lem  26988  dchrvmasumiflem1  26993  selbergb  27041  selberg2b  27044  pntibndlem3  27084  pntlem3  27101  motgrp  27783  oppnid  27986  sspnv  29966  lnof  29995  bloln  30024  dfmgc2  32153  fldexttr  32725  reff  32807  signsply0  33550  cvmliftmolem1  34260  cvmlift2lem9a  34282  gg-dvcnp2  35162  mbfresfi  36522  itg2gt0cn  36531  ismtyres  36664  ghomf  36746  rngoisohom  36836  pridlidl  36891  pridlnr  36892  maxidlidl  36897  lflf  37921  lkrcl  37950  cvrlt  38128  cvrle  38136  atbase  38147  llnbase  38368  lplnbase  38393  lvolbase  38437  psubssat  38613  lhpbase  38857  laut1o  38944  ldillaut  38970  ltrnldil  38981  diadmclN  39896  pell1234qrre  41575  lnmlsslnm  41808  cantnf2  42060  naddcnfid1  42102  cvgdvgrat  43057  stoweidlem34  44736  mpbiran3d  47435