Theorem bitr2d 188

Description: Deduction form of bitr2i 184. (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 187	. 2 |- ( ph -> ( ps <-> th ) )
4	3	bicomd 140	1 |- ( ph -> ( th <-> ps ) )

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

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  3bitrrd  214  3bitr2rd  216  pm5.18dc  869  drex1  1775  elrnmpt1  4830  xpopth  6114  sbcopeq1a  6125  ltnnnq  7322  ltaddsub  8290  leaddsub  8292  posdif  8309  lesub1  8310  ltsub1  8312  lesub0  8333  possumd  8423  subap0  8497  ltdivmul  8726  ledivmul  8727  zlem1lt  9202  zltlem1  9203  negelrp  9572  fzrev2  9965  fz1sbc  9976  elfzp1b  9977  qtri3or  10120  sumsqeq0  10475  sqrtle  10913  sqrtlt  10914  absgt0ap  10976  iser3shft  11220  dvdssubr  11706  gcdn0gt0  11833  divgcdcoprmex  11950  lmbrf  12554  logge0b  13150  loggt0b  13151  logle1b  13152  loglt1b  13153