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  1846  elrnmpt1  4989  xpopth  6348  sbcopeq1a  6359  ltnnnq  7686  ltaddsub  8659  leaddsub  8661  posdif  8678  lesub1  8679  ltsub1  8681  lesub0  8702  possumd  8792  subap0  8866  ltdivmul  9099  ledivmul  9100  zlem1lt  9579  zltlem1  9580  negelrp  9965  fzrev2  10363  fz1sbc  10374  elfzp1b  10375  qtri3or  10544  sumsqeq0  10924  sqrtle  11657  sqrtlt  11658  absgt0ap  11720  iser3shft  11967  dvdssubr  12461  gcdn0gt0  12610  divgcdcoprmex  12735  pcfac  12984  gsumfzval  13535  lmbrf  15006  logge0b  15681  loggt0b  15682  logle1b  15683  loglt1b  15684  lgsne0  15837  lgsprme0  15841