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 1926  pwundif 2817  poirr 2836  cnvuni 3290  fopabap 3826  f1ofv 3862  snec 4280  map1 4411  fiint 4534  aceq5lem3 4709  elznn0 6096  cmbr2 9456

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