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  5510  fsnex  7303  fisupg  9322  fiinfg  9537  cantnff  9712  fseqenlem2  10063  fpwwe2lem10  10678  fpwwe2lem11  10679  fpwwe2  10681  rlimsqzlem  15682  ramub1lem2  17061  mriss  17680  invfun  17812  pltle  18391  subgslw  19649  frgpnabllem2  19907  cyggeninv  19916  ablfaclem3  20122  lmodfopnelem1  20913  pjff  21750  pjf2  21752  pjfo  21753  pjcss  21754  mplind  22112  mhpmpl  22166  fvmptnn04ifc  22874  chfacfisf  22876  chfacfisfcpmat  22877  tg1  22987  cldss  23053  cnf2  23273  cncnp  23304  lly1stc  23520  refbas  23534  qtoptop2  23723  qtoprest  23741  elfm3  23974  flfelbas  24018  cnextf  24090  restutopopn  24263  cfilufbas  24314  fmucnd  24317  blgt0  24425  xblss2ps  24427  xblss2  24428  tngngp  24691  cfilfil  25315  iscau2  25325  caufpm  25330  cmetcaulem  25336  dvcnp2  25970  dvcnp2OLD  25971  dvfsumrlim  26087  dvfsumrlim2  26088  fta1g  26224  dvdsflsumcom  27246  fsumvma  27272  vmadivsumb  27542  dchrisumlema  27547  dchrvmasumlem1  27554  dchrvmasum2lem  27555  dchrvmasumiflem1  27560  selbergb  27608  selberg2b  27611  pntibndlem3  27651  pntlem3  27668  motgrp  28566  oppnid  28769  sspnv  30755  lnof  30784  bloln  30813  dfmgc2  32971  ssdifidllem  33464  rprmcl  33526  rprmnz  33528  rprmnunit  33529  ply1unit  33580  fldexttr  33686  algextdeglem8  33730  reff  33800  signsply0  34545  cvmliftmolem1  35266  cvmlift2lem9a  35288  mbfresfi  37653  itg2gt0cn  37662  ismtyres  37795  ghomf  37877  rngoisohom  37967  pridlidl  38022  pridlnr  38023  maxidlidl  38028  lflf  39045  lkrcl  39074  cvrlt  39252  cvrle  39260  atbase  39271  llnbase  39492  lplnbase  39517  lvolbase  39561  psubssat  39737  lhpbase  39981  laut1o  40068  ldillaut  40094  ltrnldil  40105  diadmclN  41020  pell1234qrre  42840  lnmlsslnm  43070  cantnf2  43315  naddcnfid1  43357  cvgdvgrat  44309  stoweidlem34  45990  mpbiran3d  48646