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  868  drex1  1770  elrnmpt1  4785  xpopth  6067  sbcopeq1a  6078  ltnnnq  7224  ltaddsub  8191  leaddsub  8193  posdif  8210  lesub1  8211  ltsub1  8213  lesub0  8234  possumd  8324  subap0  8398  ltdivmul  8627  ledivmul  8628  zlem1lt  9103  zltlem1  9104  negelrp  9468  fzrev2  9858  fz1sbc  9869  elfzp1b  9870  qtri3or  10013  sumsqeq0  10364  sqrtle  10801  sqrtlt  10802  absgt0ap  10864  iser3shft  11108  dvdssubr  11528  gcdn0gt0  11655  divgcdcoprmex  11772  lmbrf  12373