Theorem 3bitrri 287

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 265	. 2 |- ( ch <-> ph )
5	1, 4	bitr3i 266	1 |- ( th <-> ph )

Syntax hints:   <-> wb 196

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 197

This theorem is referenced by:  nbbn  373  pm5.17  932  dn1  1008  2sb6rf  2452  reu8  3402  unass  3770  ssin  3835  difab  3896  csbab  4008  iunss  4561  poirr  5046  elvvv  5178  cnvuni  5309  dfco2  5634  resin  6158  dffv2  6271  dff1o6  6531  sbthcl  8082  fiint  8237  rankf  8657  dfac3  8944  dfac5lem3  8948  elznn0  11392  elnn1uz2  11765  lsmspsn  19084  nbgrel  26238  h2hlm  27837  cmbr2i  28455  pjss2i  28539  iuninc  29379  dffr5  31643  brsset  31996  brtxpsd  32001  ellines  32259  itg2addnclem3  33463  dvasin  33496  cvlsupr3  34631  dihglb2  36631  ifpidg  37836  ss2iundf  37951  dffrege76  38233  dffrege99  38256  ntrneikb  38392  iunssf  39263  disjinfi  39380