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  888  drex1  1844  elrnmpt1  4971  xpopth  6312  sbcopeq1a  6323  ltnnnq  7598  ltaddsub  8571  leaddsub  8573  posdif  8590  lesub1  8591  ltsub1  8593  lesub0  8614  possumd  8704  subap0  8778  ltdivmul  9011  ledivmul  9012  zlem1lt  9491  zltlem1  9492  negelrp  9871  fzrev2  10269  fz1sbc  10280  elfzp1b  10281  qtri3or  10447  sumsqeq0  10827  sqrtle  11533  sqrtlt  11534  absgt0ap  11596  iser3shft  11843  dvdssubr  12336  gcdn0gt0  12485  divgcdcoprmex  12610  pcfac  12859  gsumfzval  13410  lmbrf  14874  logge0b  15549  loggt0b  15550  logle1b  15551  loglt1b  15552  lgsne0  15702  lgsprme0  15706