Theorem bitr2d 188

Description: Deduction form of bitr2i 184. (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 187	. 2 |- ( ph -> ( ps <-> th ) )
4	3	bicomd 140	1 |- ( ph -> ( th <-> ps ) )

Syntax hints:   -> wi 4   <-> wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  3bitrrd  214  3bitr2rd  216  pm5.18dc  873  drex1  1786  elrnmpt1  4855  xpopth  6144  sbcopeq1a  6155  ltnnnq  7364  ltaddsub  8334  leaddsub  8336  posdif  8353  lesub1  8354  ltsub1  8356  lesub0  8377  possumd  8467  subap0  8541  ltdivmul  8771  ledivmul  8772  zlem1lt  9247  zltlem1  9248  negelrp  9623  fzrev2  10020  fz1sbc  10031  elfzp1b  10032  qtri3or  10178  sumsqeq0  10533  sqrtle  10978  sqrtlt  10979  absgt0ap  11041  iser3shft  11287  dvdssubr  11779  gcdn0gt0  11911  divgcdcoprmex  12034  pcfac  12280  lmbrf  12855  logge0b  13451  loggt0b  13452  logle1b  13453  loglt1b  13454  lgsne0  13579  lgsprme0  13583