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  2358  sb8f  2359  dfeumo  2537  2ex2rexrot  3273  sbralie  3316  sbralieALT  3317  sbralieOLD  3318  ceqsralt  3465  reu8  3680  sbcimdv  3798  sbcg  3802  unass  4113  ssin  4180  difab  4251  csbab  4381  ralidm  4458  iunssf  4986  iunssfOLD  4987  iunss  4988  iunssOLD  4989  poirr  5542  elvvv  5698  cnvuni  5833  dfco2  6201  resin  6794  dffv2  6927  dff1o6  7221  fsplit  8058  naddasslem1  8621  naddasslem2  8622  sbthcl  9028  fiint  9228  rankf  9707  dfac3  10032  dfac5lem3  10036  elznn0  12528  elnn1uz2  12864  lsmspsn  21069  elold  27870  elzs2  28410  cmbr2i  31687  pjss2i  31771  iuninc  32650  fineqvrep  35279  dffr5  35957  brsset  36090  brtxpsd  36095  ellines  36355  axtco  36674  axtco1g  36679  itg2addnclem3  38005  dvasin  38036  cvlsupr3  39801  dihglb2  41799  oneptri  43700  faosnf0.11b  43869  ifpidg  43933  dfsucon  43965  iscard4  43975  dffrege76  44381  dffrege99  44404  ntrneikb  44536  disjinfi  45637  2arwcatlem1  50067