Theorem simprbda 498

Description: Deduction eliminating a conjunct. (Contributed by NM, 22-Oct-2007.)

Hypothesis

Ref	Expression
simplbda.1	⊢ (𝜑 → (𝜓 ↔ (𝜒 ∧ 𝜃)))

Assertion

Ref	Expression
simprbda	⊢ ((𝜑 ∧ 𝜓) → 𝜒)

Proof of Theorem simprbda

Step	Hyp	Ref	Expression
1		simplbda.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  5456  fsnex  7239  fisupg  9200  fiinfg  9416  cantnff  9595  fseqenlem2  9947  fpwwe2lem10  10563  fpwwe2lem11  10564  fpwwe2  10566  rlimsqzlem  15584  ramub1lem2  16967  mriss  17570  invfun  17700  pltle  18266  subgslw  19557  frgpnabllem2  19815  cyggeninv  19824  ablfaclem3  20030  lmodfopnelem1  20861  pjff  21679  pjf2  21681  pjfo  21682  pjcss  21683  mplind  22037  mhpmpl  22099  fvmptnn04ifc  22808  chfacfisf  22810  chfacfisfcpmat  22811  tg1  22920  cldss  22985  cnf2  23205  cncnp  23236  lly1stc  23452  refbas  23466  qtoptop2  23655  qtoprest  23673  elfm3  23906  flfelbas  23950  cnextf  24022  restutopopn  24194  cfilufbas  24244  fmucnd  24247  blgt0  24355  xblss2ps  24357  xblss2  24358  tngngp  24610  cfilfil  25235  iscau2  25245  caufpm  25250  cmetcaulem  25256  dvcnp2  25889  dvcnp2OLD  25890  dvfsumrlim  26006  dvfsumrlim2  26007  fta1g  26143  dvdsflsumcom  27166  fsumvma  27192  vmadivsumb  27462  dchrisumlema  27467  dchrvmasumlem1  27474  dchrvmasum2lem  27475  dchrvmasumiflem1  27480  selbergb  27528  selberg2b  27531  pntibndlem3  27571  pntlem3  27588  motgrp  28627  oppnid  28830  sspnv  30813  lnof  30842  bloln  30871  dfmgc2  33088  elrgspnsubrunlem2  33341  ssdifidllem  33548  rprmcl  33610  rprmnz  33612  rprmnunit  33613  ply1unit  33667  fldexttr  33835  algextdeglem8  33901  reff  34016  signsply0  34728  cvmliftmolem1  35494  cvmlift2lem9a  35516  mbfresfi  37906  itg2gt0cn  37915  ismtyres  38048  ghomf  38130  rngoisohom  38220  pridlidl  38275  pridlnr  38276  maxidlidl  38281  lflf  39428  lkrcl  39457  cvrlt  39635  cvrle  39643  atbase  39654  llnbase  39874  lplnbase  39899  lvolbase  39943  psubssat  40119  lhpbase  40363  laut1o  40450  ldillaut  40476  ltrnldil  40487  diadmclN  41402  pell1234qrre  43198  lnmlsslnm  43427  cantnf2  43671  naddcnfid1  43713  cvgdvgrat  44658  stoweidlem34  46381  mpbiran3d  49145