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  5447  fsnex  7224  fisupg  9193  fiinfg  9410  cantnff  9589  fseqenlem2  9938  fpwwe2lem10  10553  fpwwe2lem11  10554  fpwwe2  10556  rlimsqzlem  15574  ramub1lem2  16957  mriss  17559  invfun  17689  pltle  18255  subgslw  19513  frgpnabllem2  19771  cyggeninv  19780  ablfaclem3  19986  lmodfopnelem1  20819  pjff  21637  pjf2  21639  pjfo  21640  pjcss  21641  mplind  21993  mhpmpl  22047  fvmptnn04ifc  22755  chfacfisf  22757  chfacfisfcpmat  22758  tg1  22867  cldss  22932  cnf2  23152  cncnp  23183  lly1stc  23399  refbas  23413  qtoptop2  23602  qtoprest  23620  elfm3  23853  flfelbas  23897  cnextf  23969  restutopopn  24142  cfilufbas  24192  fmucnd  24195  blgt0  24303  xblss2ps  24305  xblss2  24306  tngngp  24558  cfilfil  25183  iscau2  25193  caufpm  25198  cmetcaulem  25204  dvcnp2  25837  dvcnp2OLD  25838  dvfsumrlim  25954  dvfsumrlim2  25955  fta1g  26091  dvdsflsumcom  27114  fsumvma  27140  vmadivsumb  27410  dchrisumlema  27415  dchrvmasumlem1  27422  dchrvmasum2lem  27423  dchrvmasumiflem1  27428  selbergb  27476  selberg2b  27479  pntibndlem3  27519  pntlem3  27536  motgrp  28506  oppnid  28709  sspnv  30688  lnof  30717  bloln  30746  dfmgc2  32951  elrgspnsubrunlem2  33198  ssdifidllem  33403  rprmcl  33465  rprmnz  33467  rprmnunit  33468  ply1unit  33520  fldexttr  33630  algextdeglem8  33690  reff  33805  signsply0  34518  cvmliftmolem1  35253  cvmlift2lem9a  35275  mbfresfi  37645  itg2gt0cn  37654  ismtyres  37787  ghomf  37869  rngoisohom  37959  pridlidl  38014  pridlnr  38015  maxidlidl  38020  lflf  39041  lkrcl  39070  cvrlt  39248  cvrle  39256  atbase  39267  llnbase  39488  lplnbase  39513  lvolbase  39557  psubssat  39733  lhpbase  39977  laut1o  40064  ldillaut  40090  ltrnldil  40101  diadmclN  41016  pell1234qrre  42825  lnmlsslnm  43054  cantnf2  43298  naddcnfid1  43340  cvgdvgrat  44286  stoweidlem34  46016  mpbiran3d  48769