Theorem bitr2d 189

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

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

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  3bitrrd  215  3bitr2rd  217  pm5.18dc  891  drex1  1847  elrnmpt1  5007  xpopth  6369  sbcopeq1a  6380  ltnnnq  7737  ltaddsub  8709  leaddsub  8711  posdif  8728  lesub1  8729  ltsub1  8731  lesub0  8752  possumd  8842  subap0  8916  ltdivmul  9149  ledivmul  9150  zlem1lt  9633  zltlem1  9634  negelrp  10019  fzrev2  10418  fz1sbc  10429  elfzp1b  10430  qtri3or  10599  sumsqeq0  10979  sqrtle  11717  sqrtlt  11718  absgt0ap  11780  iser3shft  12027  dvdssubr  12521  gcdn0gt0  12670  divgcdcoprmex  12795  pcfac  13044  gsumfzval  13596  lmbrf  15072  logge0b  15747  loggt0b  15748  logle1b  15749  loglt1b  15750  lgsne0  15903  lgsprme0  15907