Theorem simprbda 502

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

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

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 400

This theorem is referenced by:  elrabi  3623  oteqex  5355  fsnex  7017  fisupg  8750  fiinfg  8947  cantnff  9121  fseqenlem2  9436  fpwwe2lem11  10051  fpwwe2lem12  10052  fpwwe2  10054  rlimsqzlem  14997  ramub1lem2  16353  mriss  16898  invfun  17026  pltle  17563  subgslw  18733  frgpnabllem2  18987  cyggeninv  18995  ablfaclem3  19202  lmodfopnelem1  19663  pjff  20401  pjf2  20403  pjfo  20404  pjcss  20405  psrbagf  20603  mplind  20741  mhpmpl  20795  fvmptnn04ifc  21457  chfacfisf  21459  chfacfisfcpmat  21460  tg1  21569  cldss  21634  cnf2  21854  cncnp  21885  lly1stc  22101  refbas  22115  qtoptop2  22304  qtoprest  22322  elfm3  22555  flfelbas  22599  cnextf  22671  restutopopn  22844  cfilufbas  22895  fmucnd  22898  blgt0  23006  xblss2ps  23008  xblss2  23009  tngngp  23260  cfilfil  23871  iscau2  23881  caufpm  23886  cmetcaulem  23892  dvcnp2  24523  dvfsumrlim  24634  dvfsumrlim2  24635  fta1g  24768  dvdsflsumcom  25773  fsumvma  25797  vmadivsumb  26067  dchrisumlema  26072  dchrvmasumlem1  26079  dchrvmasum2lem  26080  dchrvmasumiflem1  26085  selbergb  26133  selberg2b  26136  pntibndlem3  26176  pntlem3  26193  motgrp  26337  oppnid  26540  sspnv  28509  lnof  28538  bloln  28567  dfmgc2  30704  fldexttr  31136  reff  31192  signsply0  31931  cvmliftmolem1  32641  cvmlift2lem9a  32663  mbfresfi  35103  itg2gt0cn  35112  ismtyres  35246  ghomf  35328  rngoisohom  35418  pridlidl  35473  pridlnr  35474  maxidlidl  35479  lflf  36359  lkrcl  36388  cvrlt  36566  cvrle  36574  atbase  36585  llnbase  36805  lplnbase  36830  lvolbase  36874  psubssat  37050  lhpbase  37294  laut1o  37381  ldillaut  37407  ltrnldil  37418  diadmclN  38333  pell1234qrre  39793  lnmlsslnm  40025  cvgdvgrat  41017  stoweidlem34  42676