Theorem 3bitrri 300

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

Syntax hints:   ↔ wb 208

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 209

This theorem is referenced by:  nbbnOLD  386  pm5.17  1025  dn1  1069  sb8v  2384  sb8f  2385  dfeumo  2563  2ex2rexrot  3297  sbralie  3340  sbralieALT  3341  sbralieOLD  3342  ceqsralt  3488  reu8  3696  sbcimdv  3812  sbcg  3816  unass  4124  ssin  4190  difab  4262  csbab  4394  ralidm  4471  iunssf  5000  iunssfOLD  5001  iunss  5002  iunssOLD  5003  poirr  5567  elvvv  5723  cnvuni  5862  dfco2  6232  resin  6829  dffv2  6962  dff1o6  7259  fsplit  8096  naddasslem1  8665  naddasslem2  8666  sbthcl  9071  fiint  9271  rankf  9752  dfac3  10077  dfac5lem3  10081  elznn0  12583  elnn1uz2  12926  lsmspsn  21148  elold  27949  elzs2  28489  cmbr2i  31796  pjss2i  31880  iuninc  32757  fineqvrep  35407  dffr5  36101  brsset  36234  brtxpsd  36239  ellines  36499  axtco  36828  axtco1g  36833  mh-infprim2bi  36904  itg2addnclem3  38169  dvasin  38200  cvlsupr3  39965  dihglb2  41963  oneptri  43831  faosnf0.11b  44000  ifpidg  44064  dfsucon  44096  iscard4  44106  dffrege76  44512  dffrege99  44535  ntrneikb  44667  disjinfi  45767  2arwcatlem1  50213