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  5460  fsnex  7258  fisupg  9235  fiinfg  9452  cantnff  9627  fseqenlem2  9978  fpwwe2lem10  10593  fpwwe2lem11  10594  fpwwe2  10596  rlimsqzlem  15615  ramub1lem2  16998  mriss  17596  invfun  17726  pltle  18292  subgslw  19546  frgpnabllem2  19804  cyggeninv  19813  ablfaclem3  20019  lmodfopnelem1  20804  pjff  21621  pjf2  21623  pjfo  21624  pjcss  21625  mplind  21977  mhpmpl  22031  fvmptnn04ifc  22739  chfacfisf  22741  chfacfisfcpmat  22742  tg1  22851  cldss  22916  cnf2  23136  cncnp  23167  lly1stc  23383  refbas  23397  qtoptop2  23586  qtoprest  23604  elfm3  23837  flfelbas  23881  cnextf  23953  restutopopn  24126  cfilufbas  24176  fmucnd  24179  blgt0  24287  xblss2ps  24289  xblss2  24290  tngngp  24542  cfilfil  25167  iscau2  25177  caufpm  25182  cmetcaulem  25188  dvcnp2  25821  dvcnp2OLD  25822  dvfsumrlim  25938  dvfsumrlim2  25939  fta1g  26075  dvdsflsumcom  27098  fsumvma  27124  vmadivsumb  27394  dchrisumlema  27399  dchrvmasumlem1  27406  dchrvmasum2lem  27407  dchrvmasumiflem1  27412  selbergb  27460  selberg2b  27463  pntibndlem3  27503  pntlem3  27520  motgrp  28470  oppnid  28673  sspnv  30655  lnof  30684  bloln  30713  dfmgc2  32922  elrgspnsubrunlem2  33199  ssdifidllem  33427  rprmcl  33489  rprmnz  33491  rprmnunit  33492  ply1unit  33544  fldexttr  33654  algextdeglem8  33714  reff  33829  signsply0  34542  cvmliftmolem1  35268  cvmlift2lem9a  35290  mbfresfi  37660  itg2gt0cn  37669  ismtyres  37802  ghomf  37884  rngoisohom  37974  pridlidl  38029  pridlnr  38030  maxidlidl  38035  lflf  39056  lkrcl  39085  cvrlt  39263  cvrle  39271  atbase  39282  llnbase  39503  lplnbase  39528  lvolbase  39572  psubssat  39748  lhpbase  39992  laut1o  40079  ldillaut  40105  ltrnldil  40116  diadmclN  41031  pell1234qrre  42840  lnmlsslnm  43070  cantnf2  43314  naddcnfid1  43356  cvgdvgrat  44302  stoweidlem34  46032  mpbiran3d  48785