Theorem bitr2d 254

Description: Deduction form of bitr2i 250. (Contributed by NM, 9-Jun-2004.)

Hypotheses

Ref	Expression
bitr2d.1
bitr2d.2

Assertion

Ref	Expression
bitr2d

Proof of Theorem bitr2d

Step	Hyp	Ref	Expression
1		bitr2d.1	. . 3
2		bitr2d.2	. . 3
3	1, 2	bitrd 253	. 2
4	3	bicomd 201	1

Syntax hints:  ->wi 4  <->wb 184

This theorem is referenced by:  3bitrrd  280  3bitr2rd  282  pm5.18  356  sbequ12a  1994  elrnmpt1  5256  fndmdif  5991  weniso  6250  sbcopeq1a  6852  cantnffvalOLD  8103  cfss  8666  posdif  10070  lesub1  10071  lesub0  10094  ltdivmul  10442  ledivmul  10443  ledivmulOLD  10444  zlem1lt  10940  zltlem1  10941  ioon0  11584  fzn  11731  fzrev2  11772  fz1sbc  11783  elfzp1b  11784  sumsqeq0  12246  hashfzdm  12498  hashfirdm  12500  fz1isolem  12510  swrdn0  12655  sqrtle  13094  absgt0  13157  isershft  13486  incexc2  13650  dvdssubr  14027  gcdn0gt0  14160  pcfac  14418  ramval  14526  ltbwe  18137  iunocv  18712  lmbrf  19761  perfcls  19866  ovolscalem1  21924  itg2mulclem  22153  sineq0  22914  efif1olem4  22932  atanord  23258  rlimcnp2  23296  bposlem7  23565  rpvmasum2  23697  trgcgrg  23906  legov3  23984  opphllem6  24124  ebtwntg  24285  wwlkm1edg  24735  usg2spthonot0  24889  hial2eq2  26024  adjsym  26752  cnvadj  26811  eigvalcl  26880  mddmd  27220  mdslmd2i  27249  elat2  27259  negelrp  27564  xdivpnfrp  27629  isorng  27789  unitdivcld  27883  indpreima  28038  iooscon  28692  possumd  29116  pdivsq  29174  areacirclem1  30107  diophun  30707  jm2.19lem4  30934  isrnghm  32698  lincfsuppcl  33014  isat3  35032  ishlat3N  35079  cvrval5  35139  llnexchb2  35593  lhpoc2N  35739  lhprelat3N  35764  lautcnvle  35813  lautcvr  35816  ltrncnvatb  35862  cdlemb3  36332  cdlemg17h  36394  dih0vbN  37009  djhcvat42  37142  dvh4dimat  37165  mapdordlem2  37364

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