Theorem 3bitrri 299

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

Syntax hints:   ↔ wb 207

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 208

This theorem is referenced by:  nbbn  384  pm5.17  1019  dn1  1063  sb8v  2361  sb8f  2362  dfeumo  2540  2ex2rexrot  3274  sbralie  3317  sbralieALT  3318  sbralieOLD  3319  ceqsralt  3465  reu8  3674  sbcimdv  3791  sbcg  3795  unass  4101  ssin  4167  difab  4238  csbab  4368  ralidm  4445  iunssf  4972  iunssfOLD  4973  iunss  4974  iunssOLD  4975  poirr  5538  elvvv  5694  cnvuni  5828  dfco2  6196  resin  6789  dffv2  6922  dff1o6  7219  fsplit  8056  naddasslem1  8620  naddasslem2  8621  sbthcl  9027  fiint  9227  rankf  9709  dfac3  10034  dfac5lem3  10038  elznn0  12530  elnn1uz2  12866  lsmspsn  21074  elold  27869  elzs2  28409  cmbr2i  31685  pjss2i  31769  iuninc  32649  fineqvrep  35295  dffr5  35982  brsset  36115  brtxpsd  36120  ellines  36380  axtco  36699  axtco1g  36704  mh-infprim2bi  36775  itg2addnclem3  38040  dvasin  38071  cvlsupr3  39836  dihglb2  41834  oneptri  43702  faosnf0.11b  43871  ifpidg  43935  dfsucon  43967  iscard4  43977  dffrege76  44383  dffrege99  44406  ntrneikb  44538  disjinfi  45639  2arwcatlem1  50085