Theorem simprbda 623

Description: Deduction eliminating a conjunct. (Contributed by NM, 22-Oct-2007.)

Hypothesis

Ref	Expression
pm3.26bda.1

Assertion

Ref	Expression
simprbda

Proof of Theorem simprbda

Step	Hyp	Ref	Expression
1		pm3.26bda.1	. . 3
2	1	biimpa 484	. 2
3	2	simpld 459	1

Syntax hints:  ->wi 4  <->wb 184  /\wa 369

This theorem is referenced by:  elrabi  3254  oteqex  4745  fisupg  7788  cantnff  8114  fseqenlem2  8427  fpwwe2lem11  9039  fpwwe2lem12  9040  fpwwe2  9042  rlimsqzlem  13471  ramub1lem2  14545  mriss  15032  invfun  15158  pltle  15591  subgslw  16636  frgpnabllem2  16878  cyggeninv  16886  ablfaclem3  17138  psrbagf  18014  mplind  18167  pjff  18743  pjf2  18745  pjfo  18746  pjcss  18747  fvmptnn04ifc  19353  chfacfisf  19355  chfacfisfcpmat  19356  tg1  19465  cldss  19530  cnf2  19750  cncnp  19781  lly1stc  19997  refbas  20011  qtoptop2  20200  qtoprest  20218  elfm3  20451  flfelbas  20495  cnextf  20566  restutopopn  20741  cfilufbas  20792  fmucnd  20795  blgt0  20902  xblss2ps  20904  xblss2  20905  tngngp  21168  cfilfil  21706  iscau2  21716  caufpm  21721  cmetcaulem  21727  dvcnp2  22323  dvfsumrlim  22432  dvfsumrlim2  22433  fta1g  22568  dvdsflsumcom  23464  fsumvma  23488  vmadivsumb  23668  dchrisumlema  23673  dchrvmasumlem1  23680  dchrvmasum2lem  23681  dchrvmasumiflem1  23686  selbergb  23734  selberg2b  23737  pntibndlem3  23777  pntlem3  23794  motgrp  23930  oppnid  24118  clwlkiswlk  24757  sspnv  25639  lnof  25670  bloln  25699  reff  27842  signsply0  28508  cvmliftmolem1  28726  cvmlift2lem9a  28748  mbfresfi  30061  itg2gt0cn  30070  ismtyres  30304  ghomf  30344  rngoisohom  30383  pridlidl  30432  pridlnr  30433  maxidlidl  30438  pell1234qrre  30788  lnmlsslnm  31027  cvgdvgrat  31194  stoweidlem34  31816  lflf  34788  lkrcl  34817  cvrlt  34995  cvrle  35003  atbase  35014  llnbase  35233  lplnbase  35258  lvolbase  35302  psubssat  35478  lhpbase  35722  laut1o  35809  ldillaut  35835  ltrnldil  35846  diadmclN  36764

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 185  df-an 371