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  1014  dn1  1058  sb8v  2358  sb8f  2359  dfeumo  2537  2ex2rexrot  3273  sbralie  3316  sbralieALT  3317  sbralieOLD  3318  ceqsralt  3465  reu8  3680  sbcimdv  3798  sbcg  3802  unass  4113  ssin  4180  difab  4251  csbab  4381  ralidm  4458  iunssf  4986  iunssfOLD  4987  iunss  4988  iunssOLD  4989  poirr  5545  elvvv  5701  cnvuni  5836  dfco2  6204  resin  6797  dffv2  6930  dff1o6  7224  fsplit  8061  naddasslem1  8624  naddasslem2  8625  sbthcl  9031  fiint  9231  rankf  9712  dfac3  10037  dfac5lem3  10041  elznn0  12533  elnn1uz2  12869  lsmspsn  21074  elold  27868  elzs2  28408  cmbr2i  31685  pjss2i  31769  iuninc  32648  fineqvrep  35277  dffr5  35955  brsset  36088  brtxpsd  36093  ellines  36353  axtco  36672  axtco1g  36677  mh-infprim2bi  36748  itg2addnclem3  38011  dvasin  38042  cvlsupr3  39807  dihglb2  41805  oneptri  43706  faosnf0.11b  43875  ifpidg  43939  dfsucon  43971  iscard4  43981  dffrege76  44387  dffrege99  44410  ntrneikb  44542  disjinfi  45643  2arwcatlem1  50085