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  2355  sb8f  2356  dfeumo  2534  2ex2rexrot  3269  sbralie  3320  sbralieALT  3321  sbralieOLD  3322  ceqsralt  3473  reu8  3689  sbcimdv  3807  sbcg  3811  unass  4122  ssin  4189  difab  4260  csbab  4390  ralidm  4468  iunssf  4996  iunssfOLD  4997  iunss  4998  iunssOLD  4999  poirr  5542  elvvv  5698  cnvuni  5833  dfco2  6201  resin  6794  dffv2  6927  dff1o6  7219  fsplit  8057  naddasslem1  8620  naddasslem2  8621  sbthcl  9025  fiint  9225  rankf  9704  dfac3  10029  dfac5lem3  10033  elznn0  12501  elnn1uz2  12836  lsmspsn  21034  elold  27841  elzs2  28357  cmbr2i  31620  pjss2i  31704  iuninc  32584  fineqvrep  35219  dffr5  35897  brsset  36030  brtxpsd  36035  ellines  36295  itg2addnclem3  37813  dvasin  37844  cvlsupr3  39543  dihglb2  41541  oneptri  43441  faosnf0.11b  43610  ifpidg  43674  dfsucon  43706  iscard4  43716  dffrege76  44122  dffrege99  44145  ntrneikb  44277  disjinfi  45378  2arwcatlem1  49782