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  4873  xpopth  6170  sbcopeq1a  6181  ltnnnq  7400  ltaddsub  8370  leaddsub  8372  posdif  8389  lesub1  8390  ltsub1  8392  lesub0  8413  possumd  8503  subap0  8577  ltdivmul  8809  ledivmul  8810  zlem1lt  9285  zltlem1  9286  negelrp  9661  fzrev2  10058  fz1sbc  10069  elfzp1b  10070  qtri3or  10216  sumsqeq0  10571  sqrtle  11016  sqrtlt  11017  absgt0ap  11079  iser3shft  11325  dvdssubr  11817  gcdn0gt0  11949  divgcdcoprmex  12072  pcfac  12318  lmbrf  13348  logge0b  13944  loggt0b  13945  logle1b  13946  loglt1b  13947  lgsne0  14072  lgsprme0  14076