Theorem simprbda 651

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

Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383

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 196  df-an 385

This theorem is referenced by:  elrabi  3328  oteqex  4889  fsnex  6438  fisupg  8093  fiinfg  8288  cantnff  8454  fseqenlem2  8731  fpwwe2lem11  9341  fpwwe2lem12  9342  fpwwe2  9344  rlimsqzlem  14227  ramub1lem2  15569  mriss  16118  invfun  16247  pltle  16784  subgslw  17854  frgpnabllem2  18100  cyggeninv  18108  ablfaclem3  18309  lmodfopnelem1  18722  psrbagf  19186  mplind  19323  pjff  19875  pjf2  19877  pjfo  19878  pjcss  19879  fvmptnn04ifc  20476  chfacfisf  20478  chfacfisfcpmat  20479  tg1  20579  cldss  20643  cnf2  20863  cncnp  20894  lly1stc  21109  refbas  21123  qtoptop2  21312  qtoprest  21330  elfm3  21564  flfelbas  21608  cnextf  21680  restutopopn  21852  cfilufbas  21903  fmucnd  21906  blgt0  22014  xblss2ps  22016  xblss2  22017  tngngp  22268  cfilfil  22873  iscau2  22883  caufpm  22888  cmetcaulem  22894  dvcnp2  23489  dvfsumrlim  23598  dvfsumrlim2  23599  fta1g  23731  dvdsflsumcom  24714  fsumvma  24738  vmadivsumb  24972  dchrisumlema  24977  dchrvmasumlem1  24984  dchrvmasum2lem  24985  dchrvmasumiflem1  24990  selbergb  25038  selberg2b  25041  pntibndlem3  25081  pntlem3  25098  motgrp  25238  oppnid  25438  clwlkiswlk  26285  sspnv  26965  lnof  26994  bloln  27023  reff  29234  signsply0  29954  cvmliftmolem1  30517  cvmlift2lem9a  30539  mbfresfi  32626  itg2gt0cn  32635  ismtyres  32777  ghomf  32859  rngoisohom  32949  pridlidl  33004  pridlnr  33005  maxidlidl  33010  lflf  33368  lkrcl  33397  cvrlt  33575  cvrle  33583  atbase  33594  llnbase  33813  lplnbase  33838  lvolbase  33882  psubssat  34058  lhpbase  34302  laut1o  34389  ldillaut  34415  ltrnldil  34426  diadmclN  35344  pell1234qrre  36434  lnmlsslnm  36669  cvgdvgrat  37534  stoweidlem34  38927