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  811  drex1  1720  elrnmpt1  4613  xpopth  5833  sbcopeq1a  5844  ltnnnq  6675  ltaddsub  7607  leaddsub  7609  posdif  7626  lesub1  7627  ltsub1  7629  lesub0  7650  possumd  7736  ltdivmul  8021  ledivmul  8022  zlem1lt  8488  zltlem1  8489  fzrev2  9178  fz1sbc  9189  elfzp1b  9190  qtri3or  9329  sumsqeq0  9651  sqrtle  10060  sqrtlt  10061  absgt0ap  10123  dvdssubr  10386  gcdn0gt0  10513  divgcdcoprmex  10628