Theorem 3bitrri 263

Description: A chained inference from transitive law for logical equivalence. (Contributed by NM, 4-Aug-2006.)

Hypotheses

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

Assertion

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

Proof of Theorem 3bitrri

Step	Hyp	Ref	Expression
1		3bitri.3	. 2 |- (ch <-> th)
2		3bitri.1	. . 3 |- (ph <-> ps)
3		3bitri.2	. . 3 |- (ps <-> ch)
4	2, 3	bitr2i 241	. 2 |- (ch <-> ph)
5	1, 4	bitr3i 242	1 |- (th <-> ph)

Syntax hints:   <-> wb 176

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 177

This theorem is referenced by:  nbbn  347  pm5.17  858  dn1  932  sbralie  2848  reu8  3032  unass  3420  ssin  3477  difab  3523  iunss  4007  insklem  4304  eqpw1relk  4479  eqtfinrelk  4486  nnadjoin  4520  cnvuni  4895  dfco2  5080  resin  5307  dff1o6  5475  txpcofun  5803  releqel  5807  fnfullfunlem1  5856  ovcelem1  6171  tcfnex  6244  nclennlem1  6248  nnc3n3p1  6278  nchoicelem10  6298  nchoicelem16  6304  fnfreclem1  6317