Theorem 3bitrri 298

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  385  pm5.17  1009  dn1  1055  sb8v  2350  sb8f  2351  dfeumo  2537  2ex2rexrot  3235  sbralie  3406  reu8  3668  sbcimdv  3790  sbcg  3795  unass  4100  ssin  4164  difab  4234  eq0rdv  4338  csbab  4371  ralidm  4442  iunssf  4974  iunss  4975  poirr  5515  elvvv  5662  cnvuni  5795  dfco2  6149  resin  6738  dffv2  6863  dff1o6  7147  fsplit  7957  sbthcl  8882  fiint  9091  rankf  9552  dfac3  9877  dfac5lem3  9881  elznn0  12334  elnn1uz2  12665  lsmspsn  20346  cmbr2i  29958  pjss2i  30042  iuninc  30900  fineqvrep  33064  dffr5  33721  elold  34053  brsset  34191  brtxpsd  34196  ellines  34454  itg2addnclem3  35830  dvasin  35861  cvlsupr3  37358  dihglb2  39356  ifpidg  41098  dfsucon  41130  iscard4  41140  ss2iundf  41267  dffrege76  41547  dffrege99  41570  ntrneikb  41704  disjinfi  42731