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 2115  dfiin2 2578  relop 3265  dmopab3 3311  ssrnres 3467  iinon 3895  kmlem3 4739  ltmullem 5614  sqr2irrlem4 6657  cau3ir 6852  ntreq0 7650  shne0 9286  chrelat2 10200

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