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  1812  elrnmpt1  4918  xpopth  6243  sbcopeq1a  6254  ltnnnq  7507  ltaddsub  8480  leaddsub  8482  posdif  8499  lesub1  8500  ltsub1  8502  lesub0  8523  possumd  8613  subap0  8687  ltdivmul  8920  ledivmul  8921  zlem1lt  9399  zltlem1  9400  negelrp  9779  fzrev2  10177  fz1sbc  10188  elfzp1b  10189  qtri3or  10347  sumsqeq0  10727  sqrtle  11218  sqrtlt  11219  absgt0ap  11281  iser3shft  11528  dvdssubr  12021  gcdn0gt0  12170  divgcdcoprmex  12295  pcfac  12544  gsumfzval  13093  lmbrf  14535  logge0b  15210  loggt0b  15211  logle1b  15212  loglt1b  15213  lgsne0  15363  lgsprme0  15367