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  5437  fsnex  7211  fisupg  9166  fiinfg  9379  cantnff  9558  fseqenlem2  9907  fpwwe2lem10  10522  fpwwe2lem11  10523  fpwwe2  10525  rlimsqzlem  15543  ramub1lem2  16926  mriss  17528  invfun  17658  pltle  18224  subgslw  19482  frgpnabllem2  19740  cyggeninv  19749  ablfaclem3  19955  lmodfopnelem1  20785  pjff  21603  pjf2  21605  pjfo  21606  pjcss  21607  mplind  21959  mhpmpl  22013  fvmptnn04ifc  22721  chfacfisf  22723  chfacfisfcpmat  22724  tg1  22833  cldss  22898  cnf2  23118  cncnp  23149  lly1stc  23365  refbas  23379  qtoptop2  23568  qtoprest  23586  elfm3  23819  flfelbas  23863  cnextf  23935  restutopopn  24107  cfilufbas  24157  fmucnd  24160  blgt0  24268  xblss2ps  24270  xblss2  24271  tngngp  24523  cfilfil  25148  iscau2  25158  caufpm  25163  cmetcaulem  25169  dvcnp2  25802  dvcnp2OLD  25803  dvfsumrlim  25919  dvfsumrlim2  25920  fta1g  26056  dvdsflsumcom  27079  fsumvma  27105  vmadivsumb  27375  dchrisumlema  27380  dchrvmasumlem1  27387  dchrvmasum2lem  27388  dchrvmasumiflem1  27393  selbergb  27441  selberg2b  27444  pntibndlem3  27484  pntlem3  27501  motgrp  28475  oppnid  28678  sspnv  30657  lnof  30686  bloln  30715  dfmgc2  32933  elrgspnsubrunlem2  33183  ssdifidllem  33389  rprmcl  33451  rprmnz  33453  rprmnunit  33454  ply1unit  33506  fldexttr  33639  algextdeglem8  33705  reff  33820  signsply0  34532  cvmliftmolem1  35271  cvmlift2lem9a  35293  mbfresfi  37663  itg2gt0cn  37672  ismtyres  37805  ghomf  37887  rngoisohom  37977  pridlidl  38032  pridlnr  38033  maxidlidl  38038  lflf  39059  lkrcl  39088  cvrlt  39266  cvrle  39274  atbase  39285  llnbase  39505  lplnbase  39530  lvolbase  39574  psubssat  39750  lhpbase  39994  laut1o  40081  ldillaut  40107  ltrnldil  40118  diadmclN  41033  pell1234qrre  42842  lnmlsslnm  43071  cantnf2  43315  naddcnfid1  43357  cvgdvgrat  44303  stoweidlem34  46029  mpbiran3d  48795