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  5449  fsnex  7231  fisupg  9192  fiinfg  9408  cantnff  9587  fseqenlem2  9939  fpwwe2lem10  10555  fpwwe2lem11  10556  fpwwe2  10558  rlimsqzlem  15576  ramub1lem2  16959  mriss  17562  invfun  17692  pltle  18258  subgslw  19549  frgpnabllem2  19807  cyggeninv  19816  ablfaclem3  20022  lmodfopnelem1  20853  pjff  21671  pjf2  21673  pjfo  21674  pjcss  21675  mplind  22029  mhpmpl  22091  fvmptnn04ifc  22800  chfacfisf  22802  chfacfisfcpmat  22803  tg1  22912  cldss  22977  cnf2  23197  cncnp  23228  lly1stc  23444  refbas  23458  qtoptop2  23647  qtoprest  23665  elfm3  23898  flfelbas  23942  cnextf  24014  restutopopn  24186  cfilufbas  24236  fmucnd  24239  blgt0  24347  xblss2ps  24349  xblss2  24350  tngngp  24602  cfilfil  25227  iscau2  25237  caufpm  25242  cmetcaulem  25248  dvcnp2  25881  dvcnp2OLD  25882  dvfsumrlim  25998  dvfsumrlim2  25999  fta1g  26135  dvdsflsumcom  27158  fsumvma  27184  vmadivsumb  27454  dchrisumlema  27459  dchrvmasumlem1  27466  dchrvmasum2lem  27467  dchrvmasumiflem1  27472  selbergb  27520  selberg2b  27523  pntibndlem3  27563  pntlem3  27580  motgrp  28598  oppnid  28801  sspnv  30784  lnof  30813  bloln  30842  dfmgc2  33059  elrgspnsubrunlem2  33311  ssdifidllem  33518  rprmcl  33580  rprmnz  33582  rprmnunit  33583  ply1unit  33637  fldexttr  33796  algextdeglem8  33862  reff  33977  signsply0  34689  cvmliftmolem1  35456  cvmlift2lem9a  35478  mbfresfi  37838  itg2gt0cn  37847  ismtyres  37980  ghomf  38062  rngoisohom  38152  pridlidl  38207  pridlnr  38208  maxidlidl  38213  lflf  39360  lkrcl  39389  cvrlt  39567  cvrle  39575  atbase  39586  llnbase  39806  lplnbase  39831  lvolbase  39875  psubssat  40051  lhpbase  40295  laut1o  40382  ldillaut  40408  ltrnldil  40419  diadmclN  41334  pell1234qrre  43130  lnmlsslnm  43359  cantnf2  43603  naddcnfid1  43645  cvgdvgrat  44590  stoweidlem34  46314  mpbiran3d  49078