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  888  drex1  1844  elrnmpt1  4975  xpopth  6328  sbcopeq1a  6339  ltnnnq  7621  ltaddsub  8594  leaddsub  8596  posdif  8613  lesub1  8614  ltsub1  8616  lesub0  8637  possumd  8727  subap0  8801  ltdivmul  9034  ledivmul  9035  zlem1lt  9514  zltlem1  9515  negelrp  9895  fzrev2  10293  fz1sbc  10304  elfzp1b  10305  qtri3or  10472  sumsqeq0  10852  sqrtle  11563  sqrtlt  11564  absgt0ap  11626  iser3shft  11873  dvdssubr  12366  gcdn0gt0  12515  divgcdcoprmex  12640  pcfac  12889  gsumfzval  13440  lmbrf  14905  logge0b  15580  loggt0b  15581  logle1b  15582  loglt1b  15583  lgsne0  15733  lgsprme0  15737