Theorem 3bitr3r 157

Description: A chained inference from transitive law for logical equivalence.

Hypotheses

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

Assertion

Ref	Expression
3bitr3r	|- (th <-> ch)

Proof of Theorem 3bitr3r

Step	Hyp	Ref	Expression
1		3bitr3.3	. 2 |- (ps <-> th)
2		3bitr3.1	. . 3 |- (ph <-> ps)
3		3bitr3.2	. . 3 |- (ph <-> ch)
4	2, 3	bitr3 153	. 2 |- (ps <-> ch)
5	1, 4	bitr3 153	1 |- (th <-> ch)

Syntax hints:   <-> wb 127

This theorem is referenced by:  bigolden 513  ralcom4 1360  rexcom4 1361  zfpair 1891  opabid 2099  intirr 2628  dffunmof 2678  fununi 2705  tfrlem2 2950  sbthcl 3361  xpmapenlem4 3394  kmlem3 3582  ltaddsub 4320

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

This theorem depends on definitions:  df-bi 128

metamath.org