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 745  2eu6 1447  2eu8 1449  ralcom4 1814  rexcom4 1815  zfpair 2767  opabid 2799  intirr 3427  dffunmof 3516  fununi 3549  tfrlem2 3897  sbthcl 4439  xpmapenlem4 4479  abfii2 4536  kmlem3 4739  lesub0 5586  sqeqor 6578  bcpasc 6907  tgss3t 7580  nmcopexlem1 9866  nmcfnexlem1 9895

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