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  2849  reu8  3033  unass  3421  ssin  3478  difab  3524  iunss  4008  insklem  4305  eqpw1relk  4480  eqtfinrelk  4487  nnadjoin  4521  cnvuni  4896  dfco2  5081  resin  5308  dff1o6  5476  txpcofun  5804  releqel  5808  fnfullfunlem1  5857  ovcelem1  6172  tcfnex  6245  nclennlem1  6249  nnc3n3p1  6279  nchoicelem10  6299  nchoicelem16  6305  fnfreclem1  6318