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

Syntax hints:   ↔ wb 206

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 207

This theorem is referenced by:  nbbn  383  pm5.17  1014  dn1  1058  sb8v  2357  sb8f  2358  dfeumo  2536  2ex2rexrot  3272  sbralie  3315  sbralieALT  3316  sbralieOLD  3317  ceqsralt  3464  reu8  3679  sbcimdv  3797  sbcg  3801  unass  4112  ssin  4179  difab  4250  csbab  4380  ralidm  4457  iunssf  4985  iunssfOLD  4986  iunss  4987  iunssOLD  4988  poirr  5551  elvvv  5707  cnvuni  5841  dfco2  6209  resin  6802  dffv2  6935  dff1o6  7230  fsplit  8067  naddasslem1  8630  naddasslem2  8631  sbthcl  9037  fiint  9237  rankf  9718  dfac3  10043  dfac5lem3  10047  elznn0  12539  elnn1uz2  12875  lsmspsn  21079  elold  27851  elzs2  28391  cmbr2i  31667  pjss2i  31751  iuninc  32630  fineqvrep  35258  dffr5  35936  brsset  36069  brtxpsd  36074  ellines  36334  axtco  36653  axtco1g  36658  mh-infprim2bi  36729  itg2addnclem3  37994  dvasin  38025  cvlsupr3  39790  dihglb2  41788  oneptri  43685  faosnf0.11b  43854  ifpidg  43918  dfsucon  43950  iscard4  43960  dffrege76  44366  dffrege99  44389  ntrneikb  44521  disjinfi  45622  2arwcatlem1  50070