Theorem 3bitrri 301

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

Syntax hints:   ↔ wb 209

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 210

This theorem is referenced by:  nbbn  388  pm5.17  1012  dn1  1058  noranOLD  1533  dfeumo  2536  2ex2rexrot  3163  sbralie  3371  reu8  3635  sbcimdv  3756  sbcg  3761  unass  4066  ssin  4131  difab  4201  eq0rdv  4305  csbab  4338  ralidm  4409  iunssf  4939  iunss  4940  poirr  5465  elvvv  5609  cnvuni  5740  dfco2  6089  resin  6660  dffv2  6784  dff1o6  7064  fsplit  7863  sbthcl  8746  fiint  8926  rankf  9375  dfac3  9700  dfac5lem3  9704  elznn0  12156  elnn1uz2  12486  lsmspsn  20075  cmbr2i  29631  pjss2i  29715  iuninc  30573  fineqvrep  32731  dffr5  33390  elold  33739  brsset  33877  brtxpsd  33882  ellines  34140  itg2addnclem3  35516  dvasin  35547  cvlsupr3  37044  dihglb2  39042  ifpidg  40724  dfsucon  40756  iscard4  40766  ss2iundf  40885  dffrege76  41165  dffrege99  41188  ntrneikb  41322  disjinfi  42345