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-mp 5  ax-1 6  ax-2 7  ax-3 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  3173  opkelimagekg  4272  copsex2t  4609  copsex2g  4610  resieq  4980  fnssresb  5196  funimass5  5406  isocnv  5492  isoini  5498  ovmpt2x  5713  brcupg  5815  brcomposeg  5820  brcrossg  5849  enpw1  6063  enmap1lem3  6072  nenpw1pwlem2  6086  te0c  6238