Theorem simprbda 501

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  oteqex  5463  fsnex  7256  fisupg  9221  fiinfg  9437  cantnff  9619  fseqenlem2  9971  fpwwe2lem10  10588  fpwwe2lem11  10589  fpwwe2  10591  rlimsqzlem  15652  ramub1lem2  17039  mriss  17643  invfun  17773  pltle  18339  subgslw  19632  frgpnabllem2  19890  cyggeninv  19899  ablfaclem3  20105  lmodfopnelem1  20938  pjff  21737  pjf2  21739  pjfo  21740  pjcss  21741  mplind  22096  mhpmpl  22182  fvmptnn04ifc  22885  chfacfisf  22887  chfacfisfcpmat  22888  tg1  22997  cldss  23062  cnf2  23282  cncnp  23313  lly1stc  23529  refbas  23543  qtoptop2  23732  qtoprest  23750  elfm3  23983  flfelbas  24027  cnextf  24099  restutopopn  24271  cfilufbas  24321  fmucnd  24324  blgt0  24432  xblss2ps  24434  xblss2  24435  tngngp  24687  cfilfil  25302  iscau2  25312  caufpm  25317  cmetcaulem  25323  dvcnp2  25955  dvfsumrlim  26066  dvfsumrlim2  26067  fta1g  26203  dvdsflsumcom  27222  fsumvma  27247  vmadivsumb  27517  dchrisumlema  27522  dchrvmasumlem1  27529  dchrvmasum2lem  27530  dchrvmasumiflem1  27535  selbergb  27583  selberg2b  27586  pntibndlem3  27626  pntlem3  27643  motgrp  28682  oppnid  28885  sspnv  30868  lnof  30897  bloln  30926  dfmgc2  33128  elrgspnsubrunlem2  33383  ssdifidllem  33597  dflringlem2  33645  rprmcl  33668  rprmnz  33670  rprmnunit  33671  ply1unit  33725  fldexttr  33909  algextdeglem8  33975  reff  34090  signsply0  34802  cvmliftmolem1  35579  cvmlift2lem9a  35601  mbfresfi  38113  itg2gt0cn  38122  ismtyres  38255  ghomf  38337  rngoisohom  38427  pridlidl  38482  pridlnr  38483  maxidlidl  38488  lflf  39635  lkrcl  39664  cvrlt  39842  cvrle  39850  atbase  39861  llnbase  40081  lplnbase  40106  lvolbase  40150  psubssat  40326  lhpbase  40570  laut1o  40657  ldillaut  40683  ltrnldil  40694  diadmclN  41609  pell1234qrre  43377  lnmlsslnm  43606  cantnf2  43850  naddcnfid1  43892  cvgdvgrat  44837  stoweidlem34  46556  mpbiran3d  49366