Theorem simprbda 501

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  elrabi  3666  oteqex  5376  fsnex  7025  fisupg  8752  fiinfg  8949  cantnff  9123  fseqenlem2  9437  fpwwe2lem11  10048  fpwwe2lem12  10049  fpwwe2  10051  rlimsqzlem  14990  ramub1lem2  16346  mriss  16889  invfun  17017  pltle  17554  subgslw  18724  frgpnabllem2  18977  cyggeninv  18985  ablfaclem3  19192  lmodfopnelem1  19653  psrbagf  20128  mplind  20265  mhpmpl  20318  pjff  20839  pjf2  20841  pjfo  20842  pjcss  20843  fvmptnn04ifc  21443  chfacfisf  21445  chfacfisfcpmat  21446  tg1  21555  cldss  21620  cnf2  21840  cncnp  21871  lly1stc  22087  refbas  22101  qtoptop2  22290  qtoprest  22308  elfm3  22541  flfelbas  22585  cnextf  22657  restutopopn  22830  cfilufbas  22881  fmucnd  22884  blgt0  22992  xblss2ps  22994  xblss2  22995  tngngp  23246  cfilfil  23853  iscau2  23863  caufpm  23868  cmetcaulem  23874  dvcnp2  24502  dvfsumrlim  24613  dvfsumrlim2  24614  fta1g  24747  dvdsflsumcom  25751  fsumvma  25775  vmadivsumb  26045  dchrisumlema  26050  dchrvmasumlem1  26057  dchrvmasum2lem  26058  dchrvmasumiflem1  26063  selbergb  26111  selberg2b  26114  pntibndlem3  26154  pntlem3  26171  motgrp  26315  oppnid  26518  sspnv  28487  lnof  28516  bloln  28545  dfmgc2  30664  fldexttr  31058  reff  31113  signsply0  31828  cvmliftmolem1  32535  cvmlift2lem9a  32557  mbfresfi  34972  itg2gt0cn  34981  ismtyres  35118  ghomf  35200  rngoisohom  35290  pridlidl  35345  pridlnr  35346  maxidlidl  35351  lflf  36231  lkrcl  36260  cvrlt  36438  cvrle  36446  atbase  36457  llnbase  36677  lplnbase  36702  lvolbase  36746  psubssat  36922  lhpbase  37166  laut1o  37253  ldillaut  37279  ltrnldil  37290  diadmclN  38205  pell1234qrre  39541  lnmlsslnm  39773  cvgdvgrat  40735  stoweidlem34  42409