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  4354  lefinlteq  4464  funbrfv2b  5363  dffn5  5364  fnrnfv  5365  fniniseg  5372  dff13  5472  isoini  5498  caovord3  5632  ce0ncpw1  6186  cantcb  6336