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  5519  fsnex  7319  fisupg  9352  fiinfg  9568  cantnff  9743  fseqenlem2  10094  fpwwe2lem10  10709  fpwwe2lem11  10710  fpwwe2  10712  rlimsqzlem  15697  ramub1lem2  17074  mriss  17693  invfun  17825  pltle  18403  subgslw  19658  frgpnabllem2  19916  cyggeninv  19925  ablfaclem3  20131  lmodfopnelem1  20918  pjff  21755  pjf2  21757  pjfo  21758  pjcss  21759  mplind  22117  mhpmpl  22171  fvmptnn04ifc  22879  chfacfisf  22881  chfacfisfcpmat  22882  tg1  22992  cldss  23058  cnf2  23278  cncnp  23309  lly1stc  23525  refbas  23539  qtoptop2  23728  qtoprest  23746  elfm3  23979  flfelbas  24023  cnextf  24095  restutopopn  24268  cfilufbas  24319  fmucnd  24322  blgt0  24430  xblss2ps  24432  xblss2  24433  tngngp  24696  cfilfil  25320  iscau2  25330  caufpm  25335  cmetcaulem  25341  dvcnp2  25975  dvcnp2OLD  25976  dvfsumrlim  26092  dvfsumrlim2  26093  fta1g  26229  dvdsflsumcom  27249  fsumvma  27275  vmadivsumb  27545  dchrisumlema  27550  dchrvmasumlem1  27557  dchrvmasum2lem  27558  dchrvmasumiflem1  27563  selbergb  27611  selberg2b  27614  pntibndlem3  27654  pntlem3  27671  motgrp  28569  oppnid  28772  sspnv  30758  lnof  30787  bloln  30816  dfmgc2  32969  ssdifidllem  33449  rprmcl  33511  rprmnz  33513  rprmnunit  33514  ply1unit  33565  fldexttr  33671  algextdeglem8  33715  reff  33785  signsply0  34528  cvmliftmolem1  35249  cvmlift2lem9a  35271  mbfresfi  37626  itg2gt0cn  37635  ismtyres  37768  ghomf  37850  rngoisohom  37940  pridlidl  37995  pridlnr  37996  maxidlidl  38001  lflf  39019  lkrcl  39048  cvrlt  39226  cvrle  39234  atbase  39245  llnbase  39466  lplnbase  39491  lvolbase  39535  psubssat  39711  lhpbase  39955  laut1o  40042  ldillaut  40068  ltrnldil  40079  diadmclN  40994  pell1234qrre  42808  lnmlsslnm  43038  cantnf2  43287  naddcnfid1  43329  cvgdvgrat  44282  stoweidlem34  45955  mpbiran3d  48530