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  2351  sb8f  2352  dfeumo  2530  2ex2rexrot  3264  sbralie  3315  sbralieALT  3316  sbralieOLD  3317  ceqsralt  3471  reu8  3693  sbcimdv  3811  sbcg  3815  unass  4123  ssin  4190  difab  4261  eq0rdv  4358  csbab  4391  ralidm  4463  iunssf  4993  iunss  4994  poirr  5539  elvvv  5695  cnvuni  5829  dfco2  6194  resin  6786  dffv2  6918  dff1o6  7212  fsplit  8050  naddasslem1  8612  naddasslem2  8613  sbthcl  9016  fiint  9216  fiintOLD  9217  rankf  9690  dfac3  10015  dfac5lem3  10019  elznn0  12486  elnn1uz2  12826  lsmspsn  20988  elold  27783  elzs2  28292  cmbr2i  31540  pjss2i  31624  iuninc  32504  fineqvrep  35070  dffr5  35727  brsset  35863  brtxpsd  35868  ellines  36126  itg2addnclem3  37653  dvasin  37684  cvlsupr3  39323  dihglb2  41321  oneptri  43230  faosnf0.11b  43400  ifpidg  43464  dfsucon  43496  iscard4  43506  dffrege76  43912  dffrege99  43935  ntrneikb  44067  disjinfi  45170  2arwcatlem1  49580