Theorem simprbda 499

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 477	. 2 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 ∧ 𝜃))
3	2	simpld 495	1 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396

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 206  df-an 397

This theorem is referenced by:  elrabiOLD  3678  oteqex  5500  fsnex  7283  fisupg  9293  fiinfg  9496  cantnff  9671  fseqenlem2  10022  fpwwe2lem10  10637  fpwwe2lem11  10638  fpwwe2  10640  rlimsqzlem  15597  ramub1lem2  16962  mriss  17581  invfun  17713  pltle  18288  subgslw  19486  frgpnabllem2  19744  cyggeninv  19753  ablfaclem3  19959  lmodfopnelem1  20513  pjff  21273  pjf2  21275  pjfo  21276  pjcss  21277  psrbagfOLD  21478  mplind  21637  mhpmpl  21693  fvmptnn04ifc  22361  chfacfisf  22363  chfacfisfcpmat  22364  tg1  22474  cldss  22540  cnf2  22760  cncnp  22791  lly1stc  23007  refbas  23021  qtoptop2  23210  qtoprest  23228  elfm3  23461  flfelbas  23505  cnextf  23577  restutopopn  23750  cfilufbas  23801  fmucnd  23804  blgt0  23912  xblss2ps  23914  xblss2  23915  tngngp  24178  cfilfil  24791  iscau2  24801  caufpm  24806  cmetcaulem  24812  dvcnp2  25444  dvfsumrlim  25555  dvfsumrlim2  25556  fta1g  25692  dvdsflsumcom  26699  fsumvma  26723  vmadivsumb  26993  dchrisumlema  26998  dchrvmasumlem1  27005  dchrvmasum2lem  27006  dchrvmasumiflem1  27011  selbergb  27059  selberg2b  27062  pntibndlem3  27102  pntlem3  27119  motgrp  27832  oppnid  28035  sspnv  30017  lnof  30046  bloln  30075  dfmgc2  32204  fldexttr  32796  algextdeglem8  32840  reff  32888  signsply0  33631  cvmliftmolem1  34341  cvmlift2lem9a  34363  gg-dvcnp2  35243  mbfresfi  36620  itg2gt0cn  36629  ismtyres  36762  ghomf  36844  rngoisohom  36934  pridlidl  36989  pridlnr  36990  maxidlidl  36995  lflf  38019  lkrcl  38048  cvrlt  38226  cvrle  38234  atbase  38245  llnbase  38466  lplnbase  38491  lvolbase  38535  psubssat  38711  lhpbase  38955  laut1o  39042  ldillaut  39068  ltrnldil  39079  diadmclN  39994  pell1234qrre  41672  lnmlsslnm  41905  cantnf2  42157  naddcnfid1  42199  cvgdvgrat  43154  stoweidlem34  44829  mpbiran3d  47560