Theorem 3bitr2r 180

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

Hypotheses

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

Assertion

Ref	Expression
3bitr2r	|- (th <-> ph)

Proof of Theorem 3bitr2r

Step	Hyp	Ref	Expression
1		3bitr2.1	. . 3 |- (ph <-> ps)
2		3bitr2.2	. . 3 |- (ch <-> ps)
3	1, 2	bitr4 176	. 2 |- (ph <-> ch)
4		3bitr2.3	. 2 |- (ch <-> th)
5	3, 4	bitr2 174	1 |- (th <-> ph)

Syntax hints:   <-> wb 146

This theorem is referenced by:  ssrab 2121  dfiin2 2583  relop 3270  dmopab3 3317  ssrnres 3473  iinon 3901  kmlem3 4747  ltmullem 5622  sqr2irrlem4 6665  cau3ir 6860  ntreq0 7658  shne0 9309  chrelat2 10229

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