Theorem 3bitr3r 182

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 175	. 2 |- (ps <-> ch)
5	1, 4	bitr3 175	1 |- (th <-> ch)

Syntax hints:   <-> wb 146

This theorem is referenced by:  bigolden 749  2eu6 1457  2eu8 1459  ralcom4 1826  rexcom4 1827  zfpair 2783  opabid 2816  intirr 3447  dffunmof 3536  fununi 3569  tfrlem2 3918  sbthcl 4465  xpmapenlem4 4505  kmlem3 4777  lesub0 5624  sqeqor 6648  bcpasc 6969  tgss3t 7637  nmcopexlem1 9946  nmcfnexlem1 9975

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

This theorem depends on definitions:  df-bi 147

Copyright terms: Public domain