Theorem simprbda 498

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  oteqex  5445  fsnex  7226  fisupg  9182  fiinfg  9395  cantnff  9574  fseqenlem2  9926  fpwwe2lem10  10541  fpwwe2lem11  10542  fpwwe2  10544  rlimsqzlem  15566  ramub1lem2  16949  mriss  17551  invfun  17681  pltle  18247  subgslw  19538  frgpnabllem2  19796  cyggeninv  19805  ablfaclem3  20011  lmodfopnelem1  20841  pjff  21659  pjf2  21661  pjfo  21662  pjcss  21663  mplind  22015  mhpmpl  22069  fvmptnn04ifc  22777  chfacfisf  22779  chfacfisfcpmat  22780  tg1  22889  cldss  22954  cnf2  23174  cncnp  23205  lly1stc  23421  refbas  23435  qtoptop2  23624  qtoprest  23642  elfm3  23875  flfelbas  23919  cnextf  23991  restutopopn  24163  cfilufbas  24213  fmucnd  24216  blgt0  24324  xblss2ps  24326  xblss2  24327  tngngp  24579  cfilfil  25204  iscau2  25214  caufpm  25219  cmetcaulem  25225  dvcnp2  25858  dvcnp2OLD  25859  dvfsumrlim  25975  dvfsumrlim2  25976  fta1g  26112  dvdsflsumcom  27135  fsumvma  27161  vmadivsumb  27431  dchrisumlema  27436  dchrvmasumlem1  27443  dchrvmasum2lem  27444  dchrvmasumiflem1  27449  selbergb  27497  selberg2b  27500  pntibndlem3  27540  pntlem3  27557  motgrp  28531  oppnid  28734  sspnv  30717  lnof  30746  bloln  30775  dfmgc2  32988  elrgspnsubrunlem2  33226  ssdifidllem  33432  rprmcl  33494  rprmnz  33496  rprmnunit  33497  ply1unit  33549  fldexttr  33682  algextdeglem8  33748  reff  33863  signsply0  34575  cvmliftmolem1  35336  cvmlift2lem9a  35358  mbfresfi  37716  itg2gt0cn  37725  ismtyres  37858  ghomf  37940  rngoisohom  38030  pridlidl  38085  pridlnr  38086  maxidlidl  38091  lflf  39172  lkrcl  39201  cvrlt  39379  cvrle  39387  atbase  39398  llnbase  39618  lplnbase  39643  lvolbase  39687  psubssat  39863  lhpbase  40107  laut1o  40194  ldillaut  40220  ltrnldil  40231  diadmclN  41146  pell1234qrre  42959  lnmlsslnm  43188  cantnf2  43432  naddcnfid1  43474  cvgdvgrat  44420  stoweidlem34  46146  mpbiran3d  48911