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  5446  fsnex  7229  fisupg  9189  fiinfg  9405  cantnff  9584  fseqenlem2  9936  fpwwe2lem10  10552  fpwwe2lem11  10553  fpwwe2  10555  rlimsqzlem  15600  ramub1lem2  16987  mriss  17590  invfun  17720  pltle  18286  subgslw  19580  frgpnabllem2  19838  cyggeninv  19847  ablfaclem3  20053  lmodfopnelem1  20882  pjff  21700  pjf2  21702  pjfo  21703  pjcss  21704  mplind  22057  mhpmpl  22119  fvmptnn04ifc  22826  chfacfisf  22828  chfacfisfcpmat  22829  tg1  22938  cldss  23003  cnf2  23223  cncnp  23254  lly1stc  23470  refbas  23484  qtoptop2  23673  qtoprest  23691  elfm3  23924  flfelbas  23968  cnextf  24040  restutopopn  24212  cfilufbas  24262  fmucnd  24265  blgt0  24373  xblss2ps  24375  xblss2  24376  tngngp  24628  cfilfil  25243  iscau2  25253  caufpm  25258  cmetcaulem  25264  dvcnp2  25896  dvfsumrlim  26010  dvfsumrlim2  26011  fta1g  26147  dvdsflsumcom  27169  fsumvma  27195  vmadivsumb  27465  dchrisumlema  27470  dchrvmasumlem1  27477  dchrvmasum2lem  27478  dchrvmasumiflem1  27483  selbergb  27531  selberg2b  27534  pntibndlem3  27574  pntlem3  27591  motgrp  28630  oppnid  28833  sspnv  30817  lnof  30846  bloln  30875  dfmgc2  33076  elrgspnsubrunlem2  33329  ssdifidllem  33536  rprmcl  33598  rprmnz  33600  rprmnunit  33601  ply1unit  33655  fldexttr  33823  algextdeglem8  33889  reff  34004  signsply0  34716  cvmliftmolem1  35484  cvmlift2lem9a  35506  mbfresfi  37998  itg2gt0cn  38007  ismtyres  38140  ghomf  38222  rngoisohom  38312  pridlidl  38367  pridlnr  38368  maxidlidl  38373  lflf  39520  lkrcl  39549  cvrlt  39727  cvrle  39735  atbase  39746  llnbase  39966  lplnbase  39991  lvolbase  40035  psubssat  40211  lhpbase  40455  laut1o  40542  ldillaut  40568  ltrnldil  40579  diadmclN  41494  pell1234qrre  43295  lnmlsslnm  43524  cantnf2  43768  naddcnfid1  43810  cvgdvgrat  44755  stoweidlem34  46477  mpbiran3d  49269