Theorem simprbda 498

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  oteqex  5455  fsnex  7238  fisupg  9198  fiinfg  9414  cantnff  9595  fseqenlem2  9947  fpwwe2lem10  10563  fpwwe2lem11  10564  fpwwe2  10566  rlimsqzlem  15611  ramub1lem2  16998  mriss  17601  invfun  17731  pltle  18297  subgslw  19591  frgpnabllem2  19849  cyggeninv  19858  ablfaclem3  20064  lmodfopnelem1  20893  pjff  21692  pjf2  21694  pjfo  21695  pjcss  21696  mplind  22048  mhpmpl  22110  fvmptnn04ifc  22817  chfacfisf  22819  chfacfisfcpmat  22820  tg1  22929  cldss  22994  cnf2  23214  cncnp  23245  lly1stc  23461  refbas  23475  qtoptop2  23664  qtoprest  23682  elfm3  23915  flfelbas  23959  cnextf  24031  restutopopn  24203  cfilufbas  24253  fmucnd  24256  blgt0  24364  xblss2ps  24366  xblss2  24367  tngngp  24619  cfilfil  25234  iscau2  25244  caufpm  25249  cmetcaulem  25255  dvcnp2  25887  dvfsumrlim  25998  dvfsumrlim2  25999  fta1g  26135  dvdsflsumcom  27151  fsumvma  27176  vmadivsumb  27446  dchrisumlema  27451  dchrvmasumlem1  27458  dchrvmasum2lem  27459  dchrvmasumiflem1  27464  selbergb  27512  selberg2b  27515  pntibndlem3  27555  pntlem3  27572  motgrp  28611  oppnid  28814  sspnv  30797  lnof  30826  bloln  30855  dfmgc2  33056  elrgspnsubrunlem2  33309  ssdifidllem  33516  rprmcl  33578  rprmnz  33580  rprmnunit  33581  ply1unit  33635  fldexttr  33802  algextdeglem8  33868  reff  33983  signsply0  34695  cvmliftmolem1  35463  cvmlift2lem9a  35485  mbfresfi  37987  itg2gt0cn  37996  ismtyres  38129  ghomf  38211  rngoisohom  38301  pridlidl  38356  pridlnr  38357  maxidlidl  38362  lflf  39509  lkrcl  39538  cvrlt  39716  cvrle  39724  atbase  39735  llnbase  39955  lplnbase  39980  lvolbase  40024  psubssat  40200  lhpbase  40444  laut1o  40531  ldillaut  40557  ltrnldil  40568  diadmclN  41483  pell1234qrre  43280  lnmlsslnm  43509  cantnf2  43753  naddcnfid1  43795  cvgdvgrat  44740  stoweidlem34  46462  mpbiran3d  49266