Theorem 3bitrr 178

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

Hypotheses

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

Assertion

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

Proof of Theorem 3bitrr

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

Syntax hints:   <-> wb 146

This theorem is referenced by:  reu8 1933  pwundif 2824  poirr 2841  cnvuni 3297  fopabap 3836  f1ofv 3872  snec 4289  map1 4420  fiint 4543  aceq5lem3 4720  elznn0 6106  cmbr2 9496

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