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 205   ∧ 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 206  df-an 396

This theorem is referenced by:  elrabiOLD  3612  oteqex  5408  fsnex  7135  fisupg  8992  fiinfg  9188  cantnff  9362  fseqenlem2  9712  fpwwe2lem10  10327  fpwwe2lem11  10328  fpwwe2  10330  rlimsqzlem  15288  ramub1lem2  16656  mriss  17261  invfun  17393  pltle  17966  subgslw  19136  frgpnabllem2  19390  cyggeninv  19398  ablfaclem3  19605  lmodfopnelem1  20074  pjff  20829  pjf2  20831  pjfo  20832  pjcss  20833  psrbagfOLD  21032  mplind  21188  mhpmpl  21244  fvmptnn04ifc  21909  chfacfisf  21911  chfacfisfcpmat  21912  tg1  22022  cldss  22088  cnf2  22308  cncnp  22339  lly1stc  22555  refbas  22569  qtoptop2  22758  qtoprest  22776  elfm3  23009  flfelbas  23053  cnextf  23125  restutopopn  23298  cfilufbas  23349  fmucnd  23352  blgt0  23460  xblss2ps  23462  xblss2  23463  tngngp  23724  cfilfil  24336  iscau2  24346  caufpm  24351  cmetcaulem  24357  dvcnp2  24989  dvfsumrlim  25100  dvfsumrlim2  25101  fta1g  25237  dvdsflsumcom  26242  fsumvma  26266  vmadivsumb  26536  dchrisumlema  26541  dchrvmasumlem1  26548  dchrvmasum2lem  26549  dchrvmasumiflem1  26554  selbergb  26602  selberg2b  26605  pntibndlem3  26645  pntlem3  26662  motgrp  26808  oppnid  27011  sspnv  28989  lnof  29018  bloln  29047  dfmgc2  31176  fldexttr  31635  reff  31691  signsply0  32430  cvmliftmolem1  33143  cvmlift2lem9a  33165  mbfresfi  35750  itg2gt0cn  35759  ismtyres  35893  ghomf  35975  rngoisohom  36065  pridlidl  36120  pridlnr  36121  maxidlidl  36126  lflf  37004  lkrcl  37033  cvrlt  37211  cvrle  37219  atbase  37230  llnbase  37450  lplnbase  37475  lvolbase  37519  psubssat  37695  lhpbase  37939  laut1o  38026  ldillaut  38052  ltrnldil  38063  diadmclN  38978  pell1234qrre  40590  lnmlsslnm  40822  cvgdvgrat  41820  stoweidlem34  43465  mpbiran3d  46030