Theorem 3bitrri 297

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 275	. 2 ⊢ (𝜒 ↔ 𝜑)
5	1, 4	bitr3i 276	1 ⊢ (𝜃 ↔ 𝜑)

Syntax hints:   ↔ wb 205

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 206

This theorem is referenced by:  nbbn  384  pm5.17  1008  dn1  1054  noranOLD  1529  dfeumo  2537  2ex2rexrot  3180  sbralie  3395  reu8  3663  sbcimdv  3786  sbcg  3791  unass  4096  ssin  4161  difab  4231  eq0rdv  4335  csbab  4368  ralidm  4439  iunssf  4970  iunss  4971  poirr  5506  elvvv  5653  cnvuni  5784  dfco2  6138  resin  6721  dffv2  6845  dff1o6  7128  fsplit  7928  sbthcl  8835  fiint  9021  rankf  9483  dfac3  9808  dfac5lem3  9812  elznn0  12264  elnn1uz2  12594  lsmspsn  20261  cmbr2i  29859  pjss2i  29943  iuninc  30801  fineqvrep  32964  dffr5  33627  elold  33980  brsset  34118  brtxpsd  34123  ellines  34381  itg2addnclem3  35757  dvasin  35788  cvlsupr3  37285  dihglb2  39283  ifpidg  40996  dfsucon  41028  iscard4  41038  ss2iundf  41156  dffrege76  41436  dffrege99  41459  ntrneikb  41593  disjinfi  42620