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 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  oteqex  5483  fsnex  7281  fisupg  9247  fiinfg  9460  cantnff  9642  fseqenlem2  10008  fpwwe2lem10  10624  fpwwe2lem11  10625  fpwwe2  10627  rlimsqzlem  15700  ramub1lem2  17086  mriss  17690  invfun  17820  pltle  18386  subgslw  19685  frgpnabllem2  19943  cyggeninv  19952  ablfaclem3  20158  lmodfopnelem1  20998  ssdifidllem  21463  pjff  21841  pjf2  21843  pjfo  21844  pjcss  21845  mplind  22200  mhpmpl  22286  fvmptnn04ifc  22988  chfacfisf  22990  chfacfisfcpmat  22991  tg1  23100  cldss  23165  cnf2  23385  cncnp  23416  lly1stc  23632  refbas  23646  qtoptop2  23835  qtoprest  23853  elfm3  24086  flfelbas  24130  cnextf  24202  restutopopn  24374  cfilufbas  24424  fmucnd  24427  blgt0  24535  xblss2ps  24537  xblss2  24538  tngngp  24790  cfilfil  25405  iscau2  25415  caufpm  25420  cmetcaulem  25426  dvcnp2  26058  dvfsumrlim  26169  dvfsumrlim2  26170  fta1g  26306  dvdsflsumcom  27328  fsumvma  27353  vmadivsumb  27623  dchrisumlema  27628  dchrvmasumlem1  27635  dchrvmasum2lem  27636  dchrvmasumiflem1  27641  selbergb  27689  selberg2b  27692  pntibndlem3  27732  pntlem3  27749  motgrp  28788  oppnid  29002  sspnv  31044  lnof  31073  bloln  31102  dfmgc2  33282  elrgspnsubrunlem2  33534  dflringlem2  33751  rprmcl  33774  rprmnz  33776  rprmnunit  33777  ply1unit  33831  fldexttr  34014  algextdeglem8  34080  reff  34195  signsply0  34904  cvmliftmolem1  35739  cvmlift2lem9a  35761  mbfresfi  38283  itg2gt0cn  38292  ismtyres  38425  ghomf  38507  rngoisohom  38597  pridlidl  38652  pridlnr  38653  maxidlidl  38658  lflf  39805  lkrcl  39834  cvrlt  40012  cvrle  40020  atbase  40031  llnbase  40251  lplnbase  40276  lvolbase  40320  psubssat  40496  lhpbase  40740  laut1o  40827  ldillaut  40853  ltrnldil  40864  diadmclN  41779  pell1234qrre  43549  lnmlsslnm  43778  cantnf2  44022  naddcnfid1  44064  cvgdvgrat  44993  stoweidlem34  46718  mpbiran3d  49542