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  5480  fsnex  7281  fisupg  9301  fiinfg  9518  cantnff  9693  fseqenlem2  10044  fpwwe2lem10  10659  fpwwe2lem11  10660  fpwwe2  10662  rlimsqzlem  15670  ramub1lem2  17052  mriss  17652  invfun  17782  pltle  18348  subgslw  19602  frgpnabllem2  19860  cyggeninv  19869  ablfaclem3  20075  lmodfopnelem1  20860  pjff  21677  pjf2  21679  pjfo  21680  pjcss  21681  mplind  22033  mhpmpl  22087  fvmptnn04ifc  22795  chfacfisf  22797  chfacfisfcpmat  22798  tg1  22907  cldss  22972  cnf2  23192  cncnp  23223  lly1stc  23439  refbas  23453  qtoptop2  23642  qtoprest  23660  elfm3  23893  flfelbas  23937  cnextf  24009  restutopopn  24182  cfilufbas  24232  fmucnd  24235  blgt0  24343  xblss2ps  24345  xblss2  24346  tngngp  24598  cfilfil  25224  iscau2  25234  caufpm  25239  cmetcaulem  25245  dvcnp2  25878  dvcnp2OLD  25879  dvfsumrlim  25995  dvfsumrlim2  25996  fta1g  26132  dvdsflsumcom  27155  fsumvma  27181  vmadivsumb  27451  dchrisumlema  27456  dchrvmasumlem1  27463  dchrvmasum2lem  27464  dchrvmasumiflem1  27469  selbergb  27517  selberg2b  27520  pntibndlem3  27560  pntlem3  27577  motgrp  28527  oppnid  28730  sspnv  30712  lnof  30741  bloln  30770  dfmgc2  32981  elrgspnsubrunlem2  33248  ssdifidllem  33476  rprmcl  33538  rprmnz  33540  rprmnunit  33541  ply1unit  33593  fldexttr  33705  algextdeglem8  33763  reff  33875  signsply0  34588  cvmliftmolem1  35308  cvmlift2lem9a  35330  mbfresfi  37695  itg2gt0cn  37704  ismtyres  37837  ghomf  37919  rngoisohom  38009  pridlidl  38064  pridlnr  38065  maxidlidl  38070  lflf  39086  lkrcl  39115  cvrlt  39293  cvrle  39301  atbase  39312  llnbase  39533  lplnbase  39558  lvolbase  39602  psubssat  39778  lhpbase  40022  laut1o  40109  ldillaut  40135  ltrnldil  40146  diadmclN  41061  pell1234qrre  42850  lnmlsslnm  43080  cantnf2  43324  naddcnfid1  43366  cvgdvgrat  44312  stoweidlem34  46043  mpbiran3d  48756