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  5033  xpopth  6410  sbcopeq1a  6421  ltnnnq  7791  ltaddsub  8766  leaddsub  8768  posdif  8785  lesub1  8786  ltsub1  8788  lesub0  8809  possumd  8900  subap0  8974  ltdivmul  9209  ledivmul  9210  zlem1lt  9706  zltlem1  9707  negelrp  10099  fzrev2  10503  fz1sbc  10514  elfzp1b  10515  qtri3or  10686  sumsqeq0  11069  sqrtle  11817  sqrtlt  11818  absgt0ap  11881  iser3shft  12130  dvdssubr  12624  gcdn0gt0  12773  divgcdcoprmex  12898  pcfac  13151  gzsumfzval  13762  lmbrf  15368  reaplog  16022  logge0b  16045  loggt0b  16046  logle1b  16047  loglt1b  16048  lgsne0  16279  lgsprme0  16283