Theorem bitr2d 189

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

Hypotheses

Ref	Expression
bitr2d.1	|- ( ph -> ( ps <-> ch ) )
bitr2d.2	|- ( ph -> ( ch <-> th ) )

Assertion

Ref	Expression
bitr2d	|- ( ph -> ( th <-> ps ) )

Proof of Theorem bitr2d

Step	Hyp	Ref	Expression
1		bitr2d.1	. . 3 |- ( ph -> ( ps <-> ch ) )
2		bitr2d.2	. . 3 |- ( ph -> ( ch <-> th ) )
3	1, 2	bitrd 188	. 2 |- ( ph -> ( ps <-> th ) )
4	3	bicomd 141	1 |- ( ph -> ( th <-> ps ) )

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  3bitrrd  215  3bitr2rd  217  pm5.18dc  891  drex1  1847  elrnmpt1  5014  xpopth  6384  sbcopeq1a  6395  ltnnnq  7755  ltaddsub  8729  leaddsub  8731  posdif  8748  lesub1  8749  ltsub1  8751  lesub0  8772  possumd  8862  subap0  8936  ltdivmul  9171  ledivmul  9172  zlem1lt  9655  zltlem1  9656  negelrp  10042  fzrev2  10445  fz1sbc  10456  elfzp1b  10457  qtri3or  10628  sumsqeq0  11008  sqrtle  11751  sqrtlt  11752  absgt0ap  11814  iser3shft  12061  dvdssubr  12555  gcdn0gt0  12704  divgcdcoprmex  12829  pcfac  13078  gsumfzval  13659  lmbrf  15211  logge0b  15886  loggt0b  15887  logle1b  15888  loglt1b  15889  lgsne0  16042  lgsprme0  16046