Theorem bitr3d 246

Description: Deduction form of bitr3i 242. (Contributed by NM, 5-Aug-1993.)

Hypotheses

Ref	Expression
bitr3d.1	|- (ph -> (ps <-> ch))
bitr3d.2	|- (ph -> (ps <-> th))

Assertion

Ref	Expression
bitr3d	|- (ph -> (ch <-> th))

Proof of Theorem bitr3d

Step	Hyp	Ref	Expression
1		bitr3d.1	. . 3 |- (ph -> (ps <-> ch))
2	1	bicomd 192	. 2 |- (ph -> (ch <-> ps))
3		bitr3d.2	. 2 |- (ph -> (ps <-> th))
4	2, 3	bitrd 244	1 |- (ph -> (ch <-> th))

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

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8

This theorem depends on definitions:  df-bi 177

This theorem is referenced by:  3bitrrd  271  3bitr3d  274  3bitr3rd  275  biass  348  sbequ12a  1921  sbco2  2086  sbco3  2088  sbcom  2089  sb9i  2094  sbcom2  2114  sbal1  2126  sbal  2127  csbiebt  3172  opkelimagekg  4271  copsex2t  4608  copsex2g  4609  resieq  4979  fnssresb  5195  funimass5  5405  isocnv  5491  isoini  5497  ovmpt2x  5712  brcupg  5814  brcomposeg  5819  brcrossg  5848  enpw1  6062  enmap1lem3  6071  nenpw1pwlem2  6085  te0c  6237