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  883  drex1  1798  elrnmpt1  4879  xpopth  6177  sbcopeq1a  6188  ltnnnq  7422  ltaddsub  8393  leaddsub  8395  posdif  8412  lesub1  8413  ltsub1  8415  lesub0  8436  possumd  8526  subap0  8600  ltdivmul  8833  ledivmul  8834  zlem1lt  9309  zltlem1  9310  negelrp  9687  fzrev2  10085  fz1sbc  10096  elfzp1b  10097  qtri3or  10243  sumsqeq0  10599  sqrtle  11045  sqrtlt  11046  absgt0ap  11108  iser3shft  11354  dvdssubr  11846  gcdn0gt0  11979  divgcdcoprmex  12102  pcfac  12348  lmbrf  13718  logge0b  14314  loggt0b  14315  logle1b  14316  loglt1b  14317  lgsne0  14442  lgsprme0  14446