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  1013  dn1  1057  sb8v  2353  sb8f  2354  dfeumo  2535  2ex2rexrot  3296  sbralie  3356  sbralieALT  3357  ceqsralt  3514  reu8  3742  sbcimdv  3865  sbcg  3870  unass  4182  ssin  4247  difab  4316  eq0rdv  4413  csbab  4446  ralidm  4518  iunssf  5049  iunss  5050  poirr  5609  elvvv  5764  cnvuni  5900  dfco2  6267  resin  6871  dffv2  7004  dff1o6  7295  fsplit  8141  naddasslem1  8731  naddasslem2  8732  sbthcl  9134  fiint  9364  fiintOLD  9365  rankf  9832  dfac3  10159  dfac5lem3  10163  elznn0  12626  elnn1uz2  12965  lsmspsn  21101  elold  27923  elzs2  28400  cmbr2i  31625  pjss2i  31709  iuninc  32581  fineqvrep  35088  dffr5  35734  brsset  35871  brtxpsd  35876  ellines  36134  itg2addnclem3  37660  dvasin  37691  cvlsupr3  39326  dihglb2  41325  oneptri  43246  faosnf0.11b  43417  ifpidg  43481  dfsucon  43513  iscard4  43523  dffrege76  43929  dffrege99  43952  ntrneikb  44084  disjinfi  45135