Theorem 3bitrri 290

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

Syntax hints:   ↔ wb 198

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 199

This theorem is referenced by:  nbbn  376  pm5.17  994  dn1  1038  2sb6rfOLD  2418  reu8  3635  unass  4030  ssin  4093  difab  4158  csbab  4271  iunss  4833  poirr  5334  elvvv  5474  cnvuni  5604  dfco2  5935  resin  6463  dffv2  6582  dff1o6  6855  sbthcl  8431  fiint  8586  rankf  9013  dfac3  9337  dfac5lem3  9341  elznn0  11805  elnn1uz2  12136  lsmspsn  19572  cmbr2i  29148  pjss2i  29232  iuninc  30075  dffr5  32479  brsset  32841  brtxpsd  32846  ellines  33104  itg2addnclem3  34364  dvasin  34397  cvlsupr3  35903  dihglb2  37901  ifpidg  39231  ss2iundf  39345  dffrege76  39626  dffrege99  39649  ntrneikb  39785  iunssf  40752  disjinfi  40857