Theorem simprbda 504

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  oteqex  5481  fsnex  7287  fisupg  9261  fiinfg  9474  cantnff  9656  fseqenlem2  10031  fpwwe2lem10  10652  fpwwe2lem11  10653  fpwwe2  10655  rlimsqzlem  15738  ramub1lem2  17123  mriss  17727  invfun  17857  pltle  18423  subgslw  19747  frgpnabllem2  20005  cyggeninv  20014  ablfaclem3  20220  lmodfopnelem1  21086  ssdifidllem  21551  pjff  21929  pjf2  21931  pjfo  21932  pjcss  21933  mplind  22290  mhpmpl  22376  fvmptnn04ifc  23081  chfacfisf  23083  chfacfisfcpmat  23084  tg1  23193  cldss  23258  cnf2  23478  cncnp  23509  lly1stc  23726  refbas  23740  qtoptop2  23929  qtoprest  23947  elfm3  24180  flfelbas  24224  cnextf  24296  restutopopn  24468  cfilufbas  24518  fmucnd  24521  blgt0  24629  xblss2ps  24631  xblss2  24632  tngngp  24884  cfilfil  25499  iscau2  25509  caufpm  25514  cmetcaulem  25520  dvcnp2  26152  dvfsumrlim  26263  dvfsumrlim2  26264  fta1g  26400  dvdsflsumcom  27425  fsumvma  27450  vmadivsumb  27720  dchrisumlema  27725  dchrvmasumlem1  27732  dchrvmasum2lem  27733  dchrvmasumiflem1  27738  selbergb  27786  selberg2b  27789  pntibndlem3  27829  pntlem3  27846  motgrp  28886  oppnid  29102  sspnv  31208  lnof  31237  bloln  31266  dfmgc2  33438  elrgspnsubrunlem2  33690  dflringlem2  33907  rprmcl  33930  rprmnz  33932  rprmnunit  33933  ply1unit  33987  fldexttr  34170  algextdeglem8  34236  reff  34351  signsply0  35061  cvmliftmolem1  35862  cvmlift2lem9a  35884  mbfresfi  38417  itg2gt0cn  38426  ismtyres  38560  ghomf  38642  rngoisohom  38732  pridlidl  38787  pridlnr  38788  maxidlidl  38793  lflf  39938  lkrcl  39967  cvrlt  40145  cvrle  40153  atbase  40164  llnbase  40384  lplnbase  40409  lvolbase  40453  psubssat  40629  lhpbase  40873  laut1o  40960  ldillaut  40986  ltrnldil  40997  diadmclN  41912  pell1234qrre  43695  lnmlsslnm  43924  cantnf2  44168  naddcnfid1  44210  cvgdvgrat  45139  stoweidlem34  46864  mpbiran3d  49727