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  5504  fsnex  7304  fisupg  9325  fiinfg  9540  cantnff  9715  fseqenlem2  10066  fpwwe2lem10  10681  fpwwe2lem11  10682  fpwwe2  10684  rlimsqzlem  15686  ramub1lem2  17066  mriss  17679  invfun  17809  pltle  18379  subgslw  19635  frgpnabllem2  19893  cyggeninv  19902  ablfaclem3  20108  lmodfopnelem1  20897  pjff  21733  pjf2  21735  pjfo  21736  pjcss  21737  mplind  22095  mhpmpl  22149  fvmptnn04ifc  22859  chfacfisf  22861  chfacfisfcpmat  22862  tg1  22972  cldss  23038  cnf2  23258  cncnp  23289  lly1stc  23505  refbas  23519  qtoptop2  23708  qtoprest  23726  elfm3  23959  flfelbas  24003  cnextf  24075  restutopopn  24248  cfilufbas  24299  fmucnd  24302  blgt0  24410  xblss2ps  24412  xblss2  24413  tngngp  24676  cfilfil  25302  iscau2  25312  caufpm  25317  cmetcaulem  25323  dvcnp2  25956  dvcnp2OLD  25957  dvfsumrlim  26073  dvfsumrlim2  26074  fta1g  26210  dvdsflsumcom  27232  fsumvma  27258  vmadivsumb  27528  dchrisumlema  27533  dchrvmasumlem1  27540  dchrvmasum2lem  27541  dchrvmasumiflem1  27546  selbergb  27594  selberg2b  27597  pntibndlem3  27637  pntlem3  27654  motgrp  28552  oppnid  28755  sspnv  30746  lnof  30775  bloln  30804  dfmgc2  32987  elrgspnsubrunlem2  33253  ssdifidllem  33485  rprmcl  33547  rprmnz  33549  rprmnunit  33550  ply1unit  33601  fldexttr  33710  algextdeglem8  33766  reff  33839  signsply0  34567  cvmliftmolem1  35287  cvmlift2lem9a  35309  mbfresfi  37674  itg2gt0cn  37683  ismtyres  37816  ghomf  37898  rngoisohom  37988  pridlidl  38043  pridlnr  38044  maxidlidl  38049  lflf  39065  lkrcl  39094  cvrlt  39272  cvrle  39280  atbase  39291  llnbase  39512  lplnbase  39537  lvolbase  39581  psubssat  39757  lhpbase  40001  laut1o  40088  ldillaut  40114  ltrnldil  40125  diadmclN  41040  pell1234qrre  42868  lnmlsslnm  43098  cantnf2  43343  naddcnfid1  43385  cvgdvgrat  44337  stoweidlem34  46054  mpbiran3d  48722