Theorem simprbda 500

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 397

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 206  df-an 398

This theorem is referenced by:  elrabiOLD  3679  oteqex  5501  fsnex  7281  fisupg  9291  fiinfg  9494  cantnff  9669  fseqenlem2  10020  fpwwe2lem10  10635  fpwwe2lem11  10636  fpwwe2  10638  rlimsqzlem  15595  ramub1lem2  16960  mriss  17579  invfun  17711  pltle  18286  subgslw  19484  frgpnabllem2  19742  cyggeninv  19751  ablfaclem3  19957  lmodfopnelem1  20508  pjff  21267  pjf2  21269  pjfo  21270  pjcss  21271  psrbagfOLD  21472  mplind  21631  mhpmpl  21687  fvmptnn04ifc  22354  chfacfisf  22356  chfacfisfcpmat  22357  tg1  22467  cldss  22533  cnf2  22753  cncnp  22784  lly1stc  23000  refbas  23014  qtoptop2  23203  qtoprest  23221  elfm3  23454  flfelbas  23498  cnextf  23570  restutopopn  23743  cfilufbas  23794  fmucnd  23797  blgt0  23905  xblss2ps  23907  xblss2  23908  tngngp  24171  cfilfil  24784  iscau2  24794  caufpm  24799  cmetcaulem  24805  dvcnp2  25437  dvfsumrlim  25548  dvfsumrlim2  25549  fta1g  25685  dvdsflsumcom  26692  fsumvma  26716  vmadivsumb  26986  dchrisumlema  26991  dchrvmasumlem1  26998  dchrvmasum2lem  26999  dchrvmasumiflem1  27004  selbergb  27052  selberg2b  27055  pntibndlem3  27095  pntlem3  27112  motgrp  27794  oppnid  27997  sspnv  29979  lnof  30008  bloln  30037  dfmgc2  32166  fldexttr  32737  reff  32819  signsply0  33562  cvmliftmolem1  34272  cvmlift2lem9a  34294  gg-dvcnp2  35174  mbfresfi  36534  itg2gt0cn  36543  ismtyres  36676  ghomf  36758  rngoisohom  36848  pridlidl  36903  pridlnr  36904  maxidlidl  36909  lflf  37933  lkrcl  37962  cvrlt  38140  cvrle  38148  atbase  38159  llnbase  38380  lplnbase  38405  lvolbase  38449  psubssat  38625  lhpbase  38869  laut1o  38956  ldillaut  38982  ltrnldil  38993  diadmclN  39908  pell1234qrre  41590  lnmlsslnm  41823  cantnf2  42075  naddcnfid1  42117  cvgdvgrat  43072  stoweidlem34  44750  mpbiran3d  47482