Theorem simprbda 503

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

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

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 401

This theorem is used by:  oteqex  5482  fsnex  7281  fisupg  9246  fiinfg  9459  cantnff  9641  fseqenlem2  10016  fpwwe2lem10  10631  fpwwe2lem11  10632  fpwwe2  10634  rlimsqzlem  15707  ramub1lem2  17093  mriss  17697  invfun  17827  pltle  18393  subgslw  19692  frgpnabllem2  19950  cyggeninv  19959  ablfaclem3  20165  lmodfopnelem1  21030  ssdifidllem  21495  pjff  21873  pjf2  21875  pjfo  21876  pjcss  21877  mplind  22232  mhpmpl  22318  fvmptnn04ifc  23020  chfacfisf  23022  chfacfisfcpmat  23023  tg1  23132  cldss  23197  cnf2  23417  cncnp  23448  lly1stc  23664  refbas  23678  qtoptop2  23867  qtoprest  23885  elfm3  24118  flfelbas  24162  cnextf  24234  restutopopn  24406  cfilufbas  24456  fmucnd  24459  blgt0  24567  xblss2ps  24569  xblss2  24570  tngngp  24822  cfilfil  25437  iscau2  25447  caufpm  25452  cmetcaulem  25458  dvcnp2  26090  dvfsumrlim  26201  dvfsumrlim2  26202  fta1g  26338  dvdsflsumcom  27363  fsumvma  27388  vmadivsumb  27658  dchrisumlema  27663  dchrvmasumlem1  27670  dchrvmasum2lem  27671  dchrvmasumiflem1  27676  selbergb  27724  selberg2b  27727  pntibndlem3  27767  pntlem3  27784  motgrp  28823  oppnid  29038  sspnv  31089  lnof  31118  bloln  31147  dfmgc2  33325  elrgspnsubrunlem2  33577  dflringlem2  33794  rprmcl  33817  rprmnz  33819  rprmnunit  33820  ply1unit  33874  fldexttr  34057  algextdeglem8  34123  reff  34238  signsply0  34947  cvmliftmolem1  35781  cvmlift2lem9a  35803  mbfresfi  38345  itg2gt0cn  38354  ismtyres  38487  ghomf  38569  rngoisohom  38659  pridlidl  38714  pridlnr  38715  maxidlidl  38720  lflf  39865  lkrcl  39894  cvrlt  40072  cvrle  40080  atbase  40091  llnbase  40311  lplnbase  40336  lvolbase  40380  psubssat  40556  lhpbase  40800  laut1o  40887  ldillaut  40913  ltrnldil  40924  diadmclN  41839  pell1234qrre  43607  lnmlsslnm  43836  cantnf2  44080  naddcnfid1  44122  cvgdvgrat  45051  stoweidlem34  46776  mpbiran3d  49603