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  878  drex1  1791  elrnmpt1  4862  xpopth  6155  sbcopeq1a  6166  ltnnnq  7385  ltaddsub  8355  leaddsub  8357  posdif  8374  lesub1  8375  ltsub1  8377  lesub0  8398  possumd  8488  subap0  8562  ltdivmul  8792  ledivmul  8793  zlem1lt  9268  zltlem1  9269  negelrp  9644  fzrev2  10041  fz1sbc  10052  elfzp1b  10053  qtri3or  10199  sumsqeq0  10554  sqrtle  11000  sqrtlt  11001  absgt0ap  11063  iser3shft  11309  dvdssubr  11801  gcdn0gt0  11933  divgcdcoprmex  12056  pcfac  12302  lmbrf  13009  logge0b  13605  loggt0b  13606  logle1b  13607  loglt1b  13608  lgsne0  13733  lgsprme0  13737