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  1013  dn1  1057  sb8v  2351  sb8f  2352  dfeumo  2530  2ex2rexrot  3273  sbralie  3326  sbralieALT  3327  sbralieOLD  3328  ceqsralt  3482  reu8  3704  sbcimdv  3822  sbcg  3826  unass  4135  ssin  4202  difab  4273  eq0rdv  4370  csbab  4403  ralidm  4475  iunssf  5008  iunss  5009  poirr  5558  elvvv  5714  cnvuni  5850  dfco2  6218  resin  6822  dffv2  6956  dff1o6  7250  fsplit  8096  naddasslem1  8658  naddasslem2  8659  sbthcl  9063  fiint  9277  fiintOLD  9278  rankf  9747  dfac3  10074  dfac5lem3  10078  elznn0  12544  elnn1uz2  12884  lsmspsn  20991  elold  27781  elzs2  28287  cmbr2i  31525  pjss2i  31609  iuninc  32489  fineqvrep  35085  dffr5  35741  brsset  35877  brtxpsd  35882  ellines  36140  itg2addnclem3  37667  dvasin  37698  cvlsupr3  39337  dihglb2  41336  oneptri  43246  faosnf0.11b  43416  ifpidg  43480  dfsucon  43512  iscard4  43522  dffrege76  43928  dffrege99  43951  ntrneikb  44083  disjinfi  45186  2arwcatlem1  49584