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  5471  fsnex  7291  fisupg  9280  fiinfg  9494  cantnff  9676  fseqenlem2  10105  fpwwe2lem10  10726  fpwwe2lem11  10727  fpwwe2  10729  rlimsqzlem  15817  ramub1lem2  17206  mriss  17810  invfun  17940  pltle  18506  subgslw  19831  frgpnabllem2  20089  cyggeninv  20098  ablfaclem3  20304  lmodfopnelem1  21174  ssdifidllem  21641  pjff  22019  pjf2  22021  pjfo  22022  pjcss  22023  mplind  22380  mhpmpl  22466  fvmptnn04ifc  23171  chfacfisf  23173  chfacfisfcpmat  23174  tg1  23283  cldss  23348  cnf2  23568  cncnp  23599  lly1stc  23816  refbas  23830  qtoptop2  24019  qtoprest  24037  elfm3  24270  flfelbas  24314  cnextf  24386  restutopopn  24558  cfilufbas  24608  fmucnd  24611  blgt0  24719  xblss2ps  24721  xblss2  24722  tngngp  24974  cfilfil  25589  iscau2  25599  caufpm  25604  cmetcaulem  25610  dvcnp2  26241  dvfsumrlim  26352  dvfsumrlim2  26353  fta1g  26489  dvdsflsumcom  27516  fsumvma  27541  vmadivsumb  27811  dchrisumlema  27816  dchrvmasumlem1  27823  dchrvmasum2lem  27824  dchrvmasumiflem1  27829  selbergb  27877  selberg2b  27880  pntibndlem3  27920  pntlem3  27937  motgrp  29007  oppnid  29223  sspnv  31329  lnof  31358  bloln  31387  dfmgc2  33600  elrgspnsubrunlem2  33852  dflringlem2  34070  rprmcl  34093  rprmnz  34095  rprmnunit  34096  ply1unit  34150  fldexttr  34333  algextdeglem8  34399  reff  34514  signsply0  35223  cvmliftmolem1  36115  cvmlift2lem9a  36137  mbfresfi  38660  itg2gt0cn  38669  ismtyres  38818  ghomf  38900  rngoisohom  38990  pridlidl  39045  pridlnr  39046  maxidlidl  39051  lflf  40196  lkrcl  40225  cvrlt  40403  cvrle  40411  atbase  40422  llnbase  40642  lplnbase  40667  lvolbase  40711  psubssat  40887  lhpbase  41131  laut1o  41218  ldillaut  41244  ltrnldil  41255  diadmclN  42170  pell1234qrre  43935  lnmlsslnm  44159  cantnf2  44403  naddcnfid1  44445  cvgdvgrat  45373  stoweidlem34  47120  mpbiran3d  49983