Theorem simprbda 653

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

Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 384

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 197  df-an 386

This theorem is referenced by:  elrabi  3359  oteqex  4964  fsnex  6538  fisupg  8208  fiinfg  8405  cantnff  8571  fseqenlem2  8848  fpwwe2lem11  9462  fpwwe2lem12  9463  fpwwe2  9465  rlimsqzlem  14379  ramub1lem2  15731  mriss  16295  invfun  16424  pltle  16961  subgslw  18031  frgpnabllem2  18277  cyggeninv  18285  ablfaclem3  18486  lmodfopnelem1  18899  psrbagf  19365  mplind  19502  pjff  20056  pjf2  20058  pjfo  20059  pjcss  20060  fvmptnn04ifc  20657  chfacfisf  20659  chfacfisfcpmat  20660  tg1  20768  cldss  20833  cnf2  21053  cncnp  21084  lly1stc  21299  refbas  21313  qtoptop2  21502  qtoprest  21520  elfm3  21754  flfelbas  21798  cnextf  21870  restutopopn  22042  cfilufbas  22093  fmucnd  22096  blgt0  22204  xblss2ps  22206  xblss2  22207  tngngp  22458  cfilfil  23065  iscau2  23075  caufpm  23080  cmetcaulem  23086  dvcnp2  23683  dvfsumrlim  23794  dvfsumrlim2  23795  fta1g  23927  dvdsflsumcom  24914  fsumvma  24938  vmadivsumb  25172  dchrisumlema  25177  dchrvmasumlem1  25184  dchrvmasum2lem  25185  dchrvmasumiflem1  25190  selbergb  25238  selberg2b  25241  pntibndlem3  25281  pntlem3  25298  motgrp  25438  oppnid  25638  sspnv  27581  lnof  27610  bloln  27639  reff  29906  signsply0  30628  cvmliftmolem1  31263  cvmlift2lem9a  31285  mbfresfi  33456  itg2gt0cn  33465  ismtyres  33607  ghomf  33689  rngoisohom  33779  pridlidl  33834  pridlnr  33835  maxidlidl  33840  lflf  34350  lkrcl  34379  cvrlt  34557  cvrle  34565  atbase  34576  llnbase  34795  lplnbase  34820  lvolbase  34864  psubssat  35040  lhpbase  35284  laut1o  35371  ldillaut  35397  ltrnldil  35408  diadmclN  36326  pell1234qrre  37416  lnmlsslnm  37651  cvgdvgrat  38512  stoweidlem34  40251