Theorem 3bitrri 286

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

Syntax hints:   ↔ wb 195

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 196

This theorem is referenced by:  nbbn  372  pm5.17  928  dn1  1000  2sb6rf  2440  reu8  3369  unass  3732  ssin  3797  difab  3855  csbab  3960  iunss  4497  poirr  4970  elvvv  5101  cnvuni  5231  dfco2  5551  resin  6071  dffv2  6181  dff1o6  6431  sbthcl  7967  fiint  8122  rankf  8540  dfac3  8827  dfac5lem3  8831  elznn0  11269  elnn1uz2  11641  lsmspsn  18905  usg2spot2nb  26592  h2hlm  27221  cmbr2i  27839  pjss2i  27923  iuninc  28761  dffr5  30896  brsset  31166  brtxpsd  31171  ellines  31429  itg2addnclem3  32633  dvasin  32666  cvlsupr3  33649  dihglb2  35649  ifpidg  36855  ss2iundf  36970  dffrege76  37253  dffrege99  37276  ntrneikb  37412  iunssf  38290  disjinfi  38375  nbgrel  40564