Theorem simprbda 504

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  oteqex  5476  fsnex  7314  fisupg  9307  fiinfg  9520  cantnff  9702  fseqenlem2  10131  fpwwe2lem10  10752  fpwwe2lem11  10753  fpwwe2  10755  rlimsqzlem  15845  ramub1lem2  17234  mriss  17838  invfun  17968  pltle  18534  subgslw  19860  frgpnabllem2  20118  cyggeninv  20127  ablfaclem3  20333  lmodfopnelem1  21203  ssdifidllem  21670  pjff  22048  pjf2  22050  pjfo  22051  pjcss  22052  mplind  22409  mhpmpl  22495  fvmptnn04ifc  23200  chfacfisf  23202  chfacfisfcpmat  23203  tg1  23312  cldss  23377  cnf2  23597  cncnp  23628  lly1stc  23845  refbas  23859  qtoptop2  24048  qtoprest  24066  elfm3  24299  flfelbas  24343  cnextf  24415  restutopopn  24587  cfilufbas  24637  fmucnd  24640  blgt0  24748  xblss2ps  24750  xblss2  24751  tngngp  25003  cfilfil  25618  iscau2  25628  caufpm  25633  cmetcaulem  25639  dvcnp2  26270  dvfsumrlim  26381  dvfsumrlim2  26382  fta1g  26518  dvdsflsumcom  27545  fsumvma  27570  vmadivsumb  27840  dchrisumlema  27845  dchrvmasumlem1  27852  dchrvmasum2lem  27853  dchrvmasumiflem1  27858  selbergb  27906  selberg2b  27909  pntibndlem3  27949  pntlem3  27966  motgrp  29036  oppnid  29252  sspnv  31358  lnof  31387  bloln  31416  dfmgc2  33627  elrgspnsubrunlem2  33879  dflringlem2  34097  rprmcl  34120  rprmnz  34122  rprmnunit  34123  ply1unit  34177  fldexttr  34360  algextdeglem8  34426  reff  34541  signsply0  35250  k3n0k1lt  36023  cvmliftmolem1  36213  cvmlift2lem9a  36235  mbfresfi  38776  itg2gt0cn  38785  ismtyres  38934  ghomf  39016  rngoisohom  39106  pridlidl  39161  pridlnr  39162  maxidlidl  39167  lflf  40312  lkrcl  40341  cvrlt  40519  cvrle  40527  atbase  40538  llnbase  40758  lplnbase  40783  lvolbase  40827  psubssat  41003  lhpbase  41247  laut1o  41334  ldillaut  41360  ltrnldil  41371  diadmclN  42286  pell1234qrre  44052  lnmlsslnm  44276  cantnf2  44519  naddcnfid1  44561  cvgdvgrat  45489  stoweidlem34  47249  line2x  50071  mpbiran3d  50112