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:  elrabiOLD  3580  oteqex  5354  fsnex  7044  fisupg  8833  fiinfg  9029  cantnff  9203  fseqenlem2  9518  fpwwe2lem10  10133  fpwwe2lem11  10134  fpwwe2  10136  rlimsqzlem  15091  ramub1lem2  16456  mriss  17002  invfun  17132  pltle  17680  subgslw  18852  frgpnabllem2  19106  cyggeninv  19114  ablfaclem3  19321  lmodfopnelem1  19782  pjff  20521  pjf2  20523  pjfo  20524  pjcss  20525  psrbagfOLD  20725  mplind  20875  mhpmpl  20931  fvmptnn04ifc  21596  chfacfisf  21598  chfacfisfcpmat  21599  tg1  21708  cldss  21773  cnf2  21993  cncnp  22024  lly1stc  22240  refbas  22254  qtoptop2  22443  qtoprest  22461  elfm3  22694  flfelbas  22738  cnextf  22810  restutopopn  22983  cfilufbas  23034  fmucnd  23037  blgt0  23145  xblss2ps  23147  xblss2  23148  tngngp  23400  cfilfil  24012  iscau2  24022  caufpm  24027  cmetcaulem  24033  dvcnp2  24664  dvfsumrlim  24775  dvfsumrlim2  24776  fta1g  24912  dvdsflsumcom  25917  fsumvma  25941  vmadivsumb  26211  dchrisumlema  26216  dchrvmasumlem1  26223  dchrvmasum2lem  26224  dchrvmasumiflem1  26229  selbergb  26277  selberg2b  26280  pntibndlem3  26320  pntlem3  26337  motgrp  26481  oppnid  26684  sspnv  28653  lnof  28682  bloln  28711  dfmgc2  30843  fldexttr  31297  reff  31353  signsply0  32092  cvmliftmolem1  32806  cvmlift2lem9a  32828  mbfresfi  35435  itg2gt0cn  35444  ismtyres  35578  ghomf  35660  rngoisohom  35750  pridlidl  35805  pridlnr  35806  maxidlidl  35811  lflf  36689  lkrcl  36718  cvrlt  36896  cvrle  36904  atbase  36915  llnbase  37135  lplnbase  37160  lvolbase  37204  psubssat  37380  lhpbase  37624  laut1o  37711  ldillaut  37737  ltrnldil  37748  diadmclN  38663  pell1234qrre  40230  lnmlsslnm  40462  cvgdvgrat  41453  stoweidlem34  43101  monepilem  45660