Theorem simprbda 652

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

Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 383

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 197  df-an 385

This theorem is referenced by:  elrabi  3391  oteqex  4993  fsnex  6578  fisupg  8249  fiinfg  8446  cantnff  8609  fseqenlem2  8886  fpwwe2lem11  9500  fpwwe2lem12  9501  fpwwe2  9503  rlimsqzlem  14423  ramub1lem2  15778  mriss  16342  invfun  16471  pltle  17008  subgslw  18077  frgpnabllem2  18323  cyggeninv  18331  ablfaclem3  18532  lmodfopnelem1  18947  psrbagf  19413  mplind  19550  pjff  20104  pjf2  20106  pjfo  20107  pjcss  20108  fvmptnn04ifc  20705  chfacfisf  20707  chfacfisfcpmat  20708  tg1  20816  cldss  20881  cnf2  21101  cncnp  21132  lly1stc  21347  refbas  21361  qtoptop2  21550  qtoprest  21568  elfm3  21801  flfelbas  21845  cnextf  21917  restutopopn  22089  cfilufbas  22140  fmucnd  22143  blgt0  22251  xblss2ps  22253  xblss2  22254  tngngp  22505  cfilfil  23111  iscau2  23121  caufpm  23126  cmetcaulem  23132  dvcnp2  23728  dvfsumrlim  23839  dvfsumrlim2  23840  fta1g  23972  dvdsflsumcom  24959  fsumvma  24983  vmadivsumb  25217  dchrisumlema  25222  dchrvmasumlem1  25229  dchrvmasum2lem  25230  dchrvmasumiflem1  25235  selbergb  25283  selberg2b  25286  pntibndlem3  25326  pntlem3  25343  motgrp  25483  oppnid  25683  sspnv  27709  lnof  27738  bloln  27767  reff  30034  signsply0  30756  cvmliftmolem1  31389  cvmlift2lem9a  31411  mbfresfi  33586  itg2gt0cn  33595  ismtyres  33737  ghomf  33819  rngoisohom  33909  pridlidl  33964  pridlnr  33965  maxidlidl  33970  lflf  34668  lkrcl  34697  cvrlt  34875  cvrle  34883  atbase  34894  llnbase  35113  lplnbase  35138  lvolbase  35182  psubssat  35358  lhpbase  35602  laut1o  35689  ldillaut  35715  ltrnldil  35726  diadmclN  36643  pell1234qrre  37733  lnmlsslnm  37968  cvgdvgrat  38829  stoweidlem34  40569