Theorem 3bitrri 300

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

Hypotheses

Ref	Expression
3bitri.1	⊢ (𝜑 ↔ 𝜓)
3bitri.2	⊢ (𝜓 ↔ 𝜒)
3bitri.3	⊢ (𝜒 ↔ 𝜃)

Assertion

Ref	Expression
3bitrri	⊢ (𝜃 ↔ 𝜑)

Proof of Theorem 3bitrri

Step	Hyp	Ref	Expression
1		3bitri.3	. 2 ⊢ (𝜒 ↔ 𝜃)
2		3bitri.1	. . 3 ⊢ (𝜑 ↔ 𝜓)
3		3bitri.2	. . 3 ⊢ (𝜓 ↔ 𝜒)
4	2, 3	bitr2i 278	. 2 ⊢ (𝜒 ↔ 𝜑)
5	1, 4	bitr3i 279	1 ⊢ (𝜃 ↔ 𝜑)

Syntax hints:   ↔ wb 208

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 209

This theorem is referenced by:  nbbn  387  pm5.17  1008  dn1  1052  noranOLD  1523  dfeumo  2615  2ex2rexrot  3250  sbralie  3471  reu8  3723  unass  4141  ssin  4206  difab  4271  csbab  4388  iunss  4968  poirr  5484  elvvv  5626  cnvuni  5756  dfco2  6097  resin  6635  dffv2  6755  dff1o6  7031  fsplit  7811  sbthcl  8638  fiint  8794  rankf  9222  dfac3  9546  dfac5lem3  9550  elznn0  11995  elnn1uz2  12324  lsmspsn  19855  cmbr2i  29372  pjss2i  29456  iuninc  30311  dffr5  32989  brsset  33350  brtxpsd  33355  ellines  33613  itg2addnclem3  34944  dvasin  34977  cvlsupr3  36479  dihglb2  38477  ifpidg  39855  dfsucon  39887  iscard4  39898  ss2iundf  40002  dffrege76  40283  dffrege99  40306  ntrneikb  40442  iunssf  41350  disjinfi  41452