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  885  drex1  1822  elrnmpt1  4937  xpopth  6274  sbcopeq1a  6285  ltnnnq  7551  ltaddsub  8524  leaddsub  8526  posdif  8543  lesub1  8544  ltsub1  8546  lesub0  8567  possumd  8657  subap0  8731  ltdivmul  8964  ledivmul  8965  zlem1lt  9444  zltlem1  9445  negelrp  9824  fzrev2  10222  fz1sbc  10233  elfzp1b  10234  qtri3or  10400  sumsqeq0  10780  sqrtle  11417  sqrtlt  11418  absgt0ap  11480  iser3shft  11727  dvdssubr  12220  gcdn0gt0  12369  divgcdcoprmex  12494  pcfac  12743  gsumfzval  13293  lmbrf  14757  logge0b  15432  loggt0b  15433  logle1b  15434  loglt1b  15435  lgsne0  15585  lgsprme0  15589