Theorem bitr4d 247

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

Hypotheses

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

Assertion

Ref	Expression
bitr4d	|- (ph -> (ps <-> th))

Proof of Theorem bitr4d

Step	Hyp	Ref	Expression
1		bitr4d.1	. 2 |- (ph -> (ps <-> ch))
2		bitr4d.2	. . 3 |- (ph -> (th <-> ch))
3	2	bicomd 192	. 2 |- (ph -> (ch <-> th))
4	1, 3	bitrd 244	1 |- (ph -> (ps <-> 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:  3bitr2d  272  3bitr2rd  273  3bitr4d  276  3bitr4rd  277  bianabs  850  3anibar  1123  iota1  4353  lefinlteq  4463  funbrfv2b  5362  dffn5  5363  fnrnfv  5364  fniniseg  5371  dff13  5471  isoini  5497  caovord3  5631  ce0ncpw1  6185  cantcb  6335