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  4917  xpopth  6234  sbcopeq1a  6245  ltnnnq  7490  ltaddsub  8463  leaddsub  8465  posdif  8482  lesub1  8483  ltsub1  8485  lesub0  8506  possumd  8596  subap0  8670  ltdivmul  8903  ledivmul  8904  zlem1lt  9382  zltlem1  9383  negelrp  9762  fzrev2  10160  fz1sbc  10171  elfzp1b  10172  qtri3or  10330  sumsqeq0  10710  sqrtle  11201  sqrtlt  11202  absgt0ap  11264  iser3shft  11511  dvdssubr  12004  gcdn0gt0  12145  divgcdcoprmex  12270  pcfac  12519  gsumfzval  13034  lmbrf  14451  logge0b  15126  loggt0b  15127  logle1b  15128  loglt1b  15129  lgsne0  15279  lgsprme0  15283