Theorem simprbda 503

Description: Deduction eliminating a conjunct. (Contributed by NM, 22-Oct-2007.)

Hypothesis

Ref	Expression
simplbda.1	⊢ (𝜑 → (𝜓 ↔ (𝜒 ∧ 𝜃)))

Assertion

Ref	Expression
simprbda	⊢ ((𝜑 ∧ 𝜓) → 𝜒)

Proof of Theorem simprbda

Step	Hyp	Ref	Expression
1		simplbda.1	. . 3 ⊢ (𝜑 → (𝜓 ↔ (𝜒 ∧ 𝜃)))
2	1	biimpa 481	. 2 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 ∧ 𝜃))
3	2	simpld 499	1 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  oteqex  5474  fsnex  7271  fisupg  9236  fiinfg  9449  cantnff  9631  fseqenlem2  9997  fpwwe2lem10  10613  fpwwe2lem11  10614  fpwwe2  10616  rlimsqzlem  15690  ramub1lem2  17077  mriss  17681  invfun  17811  pltle  18377  subgslw  19677  frgpnabllem2  19935  cyggeninv  19944  ablfaclem3  20150  lmodfopnelem1  20988  ssdifidllem  21444  pjff  21822  pjf2  21824  pjfo  21825  pjcss  21826  mplind  22181  mhpmpl  22267  fvmptnn04ifc  22970  chfacfisf  22972  chfacfisfcpmat  22973  tg1  23082  cldss  23147  cnf2  23367  cncnp  23398  lly1stc  23614  refbas  23628  qtoptop2  23817  qtoprest  23835  elfm3  24068  flfelbas  24112  cnextf  24184  restutopopn  24356  cfilufbas  24406  fmucnd  24409  blgt0  24517  xblss2ps  24519  xblss2  24520  tngngp  24772  cfilfil  25387  iscau2  25397  caufpm  25402  cmetcaulem  25408  dvcnp2  26040  dvfsumrlim  26151  dvfsumrlim2  26152  fta1g  26288  dvdsflsumcom  27310  fsumvma  27335  vmadivsumb  27605  dchrisumlema  27610  dchrvmasumlem1  27617  dchrvmasum2lem  27618  dchrvmasumiflem1  27623  selbergb  27671  selberg2b  27674  pntibndlem3  27714  pntlem3  27731  motgrp  28770  oppnid  28977  sspnv  30987  lnof  31016  bloln  31045  dfmgc2  33229  elrgspnsubrunlem2  33481  dflringlem2  33702  rprmcl  33725  rprmnz  33727  rprmnunit  33728  ply1unit  33782  fldexttr  33965  algextdeglem8  34031  reff  34146  signsply0  34855  cvmliftmolem1  35644  cvmlift2lem9a  35666  mbfresfi  38177  itg2gt0cn  38186  ismtyres  38319  ghomf  38401  rngoisohom  38491  pridlidl  38546  pridlnr  38547  maxidlidl  38552  lflf  39699  lkrcl  39728  cvrlt  39906  cvrle  39914  atbase  39925  llnbase  40145  lplnbase  40170  lvolbase  40214  psubssat  40390  lhpbase  40634  laut1o  40721  ldillaut  40747  ltrnldil  40758  diadmclN  41673  pell1234qrre  43441  lnmlsslnm  43670  cantnf2  43914  naddcnfid1  43956  cvgdvgrat  44887  stoweidlem34  46606  mpbiran3d  49426