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  5463  fsnex  7261  fisupg  9242  fiinfg  9459  cantnff  9634  fseqenlem2  9985  fpwwe2lem10  10600  fpwwe2lem11  10601  fpwwe2  10603  rlimsqzlem  15622  ramub1lem2  17005  mriss  17603  invfun  17733  pltle  18299  subgslw  19553  frgpnabllem2  19811  cyggeninv  19820  ablfaclem3  20026  lmodfopnelem1  20811  pjff  21628  pjf2  21630  pjfo  21631  pjcss  21632  mplind  21984  mhpmpl  22038  fvmptnn04ifc  22746  chfacfisf  22748  chfacfisfcpmat  22749  tg1  22858  cldss  22923  cnf2  23143  cncnp  23174  lly1stc  23390  refbas  23404  qtoptop2  23593  qtoprest  23611  elfm3  23844  flfelbas  23888  cnextf  23960  restutopopn  24133  cfilufbas  24183  fmucnd  24186  blgt0  24294  xblss2ps  24296  xblss2  24297  tngngp  24549  cfilfil  25174  iscau2  25184  caufpm  25189  cmetcaulem  25195  dvcnp2  25828  dvcnp2OLD  25829  dvfsumrlim  25945  dvfsumrlim2  25946  fta1g  26082  dvdsflsumcom  27105  fsumvma  27131  vmadivsumb  27401  dchrisumlema  27406  dchrvmasumlem1  27413  dchrvmasum2lem  27414  dchrvmasumiflem1  27419  selbergb  27467  selberg2b  27470  pntibndlem3  27510  pntlem3  27527  motgrp  28477  oppnid  28680  sspnv  30662  lnof  30691  bloln  30720  dfmgc2  32929  elrgspnsubrunlem2  33206  ssdifidllem  33434  rprmcl  33496  rprmnz  33498  rprmnunit  33499  ply1unit  33551  fldexttr  33661  algextdeglem8  33721  reff  33836  signsply0  34549  cvmliftmolem1  35275  cvmlift2lem9a  35297  mbfresfi  37667  itg2gt0cn  37676  ismtyres  37809  ghomf  37891  rngoisohom  37981  pridlidl  38036  pridlnr  38037  maxidlidl  38042  lflf  39063  lkrcl  39092  cvrlt  39270  cvrle  39278  atbase  39289  llnbase  39510  lplnbase  39535  lvolbase  39579  psubssat  39755  lhpbase  39999  laut1o  40086  ldillaut  40112  ltrnldil  40123  diadmclN  41038  pell1234qrre  42847  lnmlsslnm  43077  cantnf2  43321  naddcnfid1  43363  cvgdvgrat  44309  stoweidlem34  46039  mpbiran3d  48789