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  884  drex1  1809  elrnmpt1  4914  xpopth  6231  sbcopeq1a  6242  ltnnnq  7485  ltaddsub  8457  leaddsub  8459  posdif  8476  lesub1  8477  ltsub1  8479  lesub0  8500  possumd  8590  subap0  8664  ltdivmul  8897  ledivmul  8898  zlem1lt  9376  zltlem1  9377  negelrp  9756  fzrev2  10154  fz1sbc  10165  elfzp1b  10166  qtri3or  10313  sumsqeq0  10692  sqrtle  11183  sqrtlt  11184  absgt0ap  11246  iser3shft  11492  dvdssubr  11985  gcdn0gt0  12118  divgcdcoprmex  12243  pcfac  12491  gsumfzval  12977  lmbrf  14394  logge0b  15066  loggt0b  15067  logle1b  15068  loglt1b  15069  lgsne0  15195  lgsprme0  15199