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  891  drex1  1847  elrnmpt1  5013  xpopth  6383  sbcopeq1a  6394  ltnnnq  7754  ltaddsub  8727  leaddsub  8729  posdif  8746  lesub1  8747  ltsub1  8749  lesub0  8770  possumd  8860  subap0  8934  ltdivmul  9167  ledivmul  9168  zlem1lt  9651  zltlem1  9652  negelrp  10038  fzrev2  10441  fz1sbc  10452  elfzp1b  10453  qtri3or  10624  sumsqeq0  11004  sqrtle  11746  sqrtlt  11747  absgt0ap  11809  iser3shft  12056  dvdssubr  12550  gcdn0gt0  12699  divgcdcoprmex  12824  pcfac  13073  gsumfzval  13688  lmbrf  15192  logge0b  15867  loggt0b  15868  logle1b  15869  loglt1b  15870  lgsne0  16023  lgsprme0  16027