Theorem bitr2d 187

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

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

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

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  3bitrrd  213  3bitr2rd  215  pm5.18dc  815  drex1  1726  elrnmpt1  4674  xpopth  5928  sbcopeq1a  5939  ltnnnq  6961  ltaddsub  7893  leaddsub  7895  posdif  7912  lesub1  7913  ltsub1  7915  lesub0  7936  possumd  8022  ltdivmul  8309  ledivmul  8310  zlem1lt  8776  zltlem1  8777  fzrev2  9466  fz1sbc  9477  elfzp1b  9478  qtri3or  9619  sumsqeq0  9997  sqrtle  10433  sqrtlt  10434  absgt0ap  10496  iser3shft  10698  dvdssubr  10922  gcdn0gt0  11049  divgcdcoprmex  11164