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 ) )

This proof depends on syntax axioms:   -> wi 4   <-> wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  3bitrrd  215  3bitr2rd  217  pm5.18dc  895  drex1  1851  elrnmpt1  5035  xpopth  6414  sbcopeq1a  6425  ltnnnq  7797  ltaddsub  8772  leaddsub  8774  posdif  8791  lesub1  8792  ltsub1  8794  lesub0  8815  possumd  8906  subap0  8980  ltdivmul  9215  ledivmul  9216  zlem1lt  9711  zltlem1  9712  negelrp  10105  fzrev2  10509  fz1sbc  10520  elfzp1b  10521  qtri3or  10692  sumsqeq0  11076  sqrtle  11824  sqrtlt  11825  absgt0ap  11888  iser3shft  12137  dvdssubr  12631  gcdn0gt0  12780  divgcdcoprmex  12905  pcfac  13158  gzsumfzval  13770  lmbrf  15474  sineq0re  16109  reaplog  16130  logge0b  16153  loggt0b  16154  logle1b  16155  loglt1b  16156  bposlem7  16350  lgsne0  16395  lgsprme0  16399