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  868  drex1  1770  elrnmpt1  4790  xpopth  6074  sbcopeq1a  6085  ltnnnq  7231  ltaddsub  8198  leaddsub  8200  posdif  8217  lesub1  8218  ltsub1  8220  lesub0  8241  possumd  8331  subap0  8405  ltdivmul  8634  ledivmul  8635  zlem1lt  9110  zltlem1  9111  negelrp  9475  fzrev2  9865  fz1sbc  9876  elfzp1b  9877  qtri3or  10020  sumsqeq0  10371  sqrtle  10808  sqrtlt  10809  absgt0ap  10871  iser3shft  11115  dvdssubr  11539  gcdn0gt0  11666  divgcdcoprmex  11783  lmbrf  12384