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  2357  sb8f  2358  dfeumo  2536  2ex2rexrot  3271  sbralie  3322  sbralieALT  3323  sbralieOLD  3324  ceqsralt  3475  reu8  3691  sbcimdv  3809  sbcg  3813  unass  4124  ssin  4191  difab  4262  csbab  4392  ralidm  4470  iunssf  4998  iunssfOLD  4999  iunss  5000  iunssOLD  5001  poirr  5544  elvvv  5700  cnvuni  5835  dfco2  6203  resin  6796  dffv2  6929  dff1o6  7221  fsplit  8059  naddasslem1  8622  naddasslem2  8623  sbthcl  9027  fiint  9227  rankf  9706  dfac3  10031  dfac5lem3  10035  elznn0  12503  elnn1uz2  12838  lsmspsn  21036  elold  27855  elzs2  28395  cmbr2i  31671  pjss2i  31755  iuninc  32635  fineqvrep  35270  dffr5  35948  brsset  36081  brtxpsd  36086  ellines  36346  itg2addnclem3  37874  dvasin  37905  cvlsupr3  39604  dihglb2  41602  oneptri  43499  faosnf0.11b  43668  ifpidg  43732  dfsucon  43764  iscard4  43774  dffrege76  44180  dffrege99  44203  ntrneikb  44335  disjinfi  45436  2arwcatlem1  49840