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  5469  fsnex  7279  fisupg  9257  fiinfg  9471  cantnff  9653  fseqenlem2  10076  fpwwe2lem10  10697  fpwwe2lem11  10698  fpwwe2  10700  rlimsqzlem  15784  ramub1lem2  17167  mriss  17771  invfun  17901  pltle  18467  subgslw  19792  frgpnabllem2  20050  cyggeninv  20059  ablfaclem3  20265  lmodfopnelem1  21135  ssdifidllem  21602  pjff  21980  pjf2  21982  pjfo  21983  pjcss  21984  mplind  22341  mhpmpl  22427  fvmptnn04ifc  23132  chfacfisf  23134  chfacfisfcpmat  23135  tg1  23244  cldss  23309  cnf2  23529  cncnp  23560  lly1stc  23777  refbas  23791  qtoptop2  23980  qtoprest  23998  elfm3  24231  flfelbas  24275  cnextf  24347  restutopopn  24519  cfilufbas  24569  fmucnd  24572  blgt0  24680  xblss2ps  24682  xblss2  24683  tngngp  24935  cfilfil  25550  iscau2  25560  caufpm  25565  cmetcaulem  25571  dvcnp2  26202  dvfsumrlim  26313  dvfsumrlim2  26314  fta1g  26450  dvdsflsumcom  27479  fsumvma  27504  vmadivsumb  27774  dchrisumlema  27779  dchrvmasumlem1  27786  dchrvmasum2lem  27787  dchrvmasumiflem1  27792  selbergb  27840  selberg2b  27843  pntibndlem3  27883  pntlem3  27900  motgrp  28940  oppnid  29156  sspnv  31262  lnof  31291  bloln  31320  dfmgc2  33491  elrgspnsubrunlem2  33743  dflringlem2  33961  rprmcl  33984  rprmnz  33986  rprmnunit  33987  ply1unit  34041  fldexttr  34224  algextdeglem8  34290  reff  34405  signsply0  35115  cvmliftmolem1  35967  cvmlift2lem9a  35989  mbfresfi  38504  itg2gt0cn  38513  ismtyres  38662  ghomf  38744  rngoisohom  38834  pridlidl  38889  pridlnr  38890  maxidlidl  38895  lflf  40040  lkrcl  40069  cvrlt  40247  cvrle  40255  atbase  40266  llnbase  40486  lplnbase  40511  lvolbase  40555  psubssat  40731  lhpbase  40975  laut1o  41062  ldillaut  41088  ltrnldil  41099  diadmclN  42014  pell1234qrre  43797  lnmlsslnm  44026  cantnf2  44270  naddcnfid1  44312  cvgdvgrat  45241  stoweidlem34  46966  mpbiran3d  49829