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  2532  2ex2rexrot  3267  sbralie  3318  sbralieALT  3319  sbralieOLD  3320  ceqsralt  3471  reu8  3687  sbcimdv  3805  sbcg  3809  unass  4117  ssin  4184  difab  4255  eq0rdv  4352  csbab  4385  ralidm  4457  iunssf  4988  iunss  4989  poirr  5531  elvvv  5687  cnvuni  5821  dfco2  6187  resin  6780  dffv2  6912  dff1o6  7204  fsplit  8042  naddasslem1  8604  naddasslem2  8605  sbthcl  9007  fiint  9206  rankf  9682  dfac3  10007  dfac5lem3  10011  elznn0  12478  elnn1uz2  12818  lsmspsn  21013  elold  27809  elzs2  28318  cmbr2i  31568  pjss2i  31652  iuninc  32532  fineqvrep  35129  dffr5  35790  brsset  35923  brtxpsd  35928  ellines  36186  itg2addnclem3  37713  dvasin  37744  cvlsupr3  39383  dihglb2  41381  oneptri  43290  faosnf0.11b  43460  ifpidg  43524  dfsucon  43556  iscard4  43566  dffrege76  43972  dffrege99  43995  ntrneikb  44127  disjinfi  45229  2arwcatlem1  49627