Theorem simprbda 494

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

Syntax hints:   → wi 4   ↔ wb 198   ∧ wa 386

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 199  df-an 387

This theorem is referenced by:  elrabi  3579  oteqex  5183  fsnex  6792  fisupg  8476  fiinfg  8673  cantnff  8847  fseqenlem2  9160  fpwwe2lem11  9776  fpwwe2lem12  9777  fpwwe2  9779  rlimsqzlem  14755  ramub1lem2  16101  mriss  16647  invfun  16775  pltle  17313  subgslw  18381  frgpnabllem2  18629  cyggeninv  18637  ablfaclem3  18839  lmodfopnelem1  19254  psrbagf  19725  mplind  19861  pjff  20418  pjf2  20420  pjfo  20421  pjcss  20422  fvmptnn04ifc  21026  chfacfisf  21028  chfacfisfcpmat  21029  tg1  21138  cldss  21203  cnf2  21423  cncnp  21454  lly1stc  21669  refbas  21683  qtoptop2  21872  qtoprest  21890  elfm3  22123  flfelbas  22167  cnextf  22239  restutopopn  22411  cfilufbas  22462  fmucnd  22465  blgt0  22573  xblss2ps  22575  xblss2  22576  tngngp  22827  cfilfil  23434  iscau2  23444  caufpm  23449  cmetcaulem  23455  dvcnp2  24081  dvfsumrlim  24192  dvfsumrlim2  24193  fta1g  24325  dvdsflsumcom  25326  fsumvma  25350  vmadivsumb  25584  dchrisumlema  25589  dchrvmasumlem1  25596  dchrvmasum2lem  25597  dchrvmasumiflem1  25602  selbergb  25650  selberg2b  25653  pntibndlem3  25693  pntlem3  25710  motgrp  25854  oppnid  26054  sspnv  28135  lnof  28164  bloln  28193  reff  30450  signsply0  31174  cvmliftmolem1  31808  cvmlift2lem9a  31830  mbfresfi  33998  itg2gt0cn  34007  ismtyres  34148  ghomf  34230  rngoisohom  34320  pridlidl  34375  pridlnr  34376  maxidlidl  34381  lflf  35137  lkrcl  35166  cvrlt  35344  cvrle  35352  atbase  35363  llnbase  35583  lplnbase  35608  lvolbase  35652  psubssat  35828  lhpbase  36072  laut1o  36159  ldillaut  36185  ltrnldil  36196  diadmclN  37111  pell1234qrre  38259  lnmlsslnm  38493  cvgdvgrat  39351  stoweidlem34  41044