Theorem 3bitrri 301

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 279	. 2 ⊢ (𝜒 ↔ 𝜑)
5	1, 4	bitr3i 280	1 ⊢ (𝜃 ↔ 𝜑)

Syntax hints:   ↔ wb 209

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 210

This theorem is referenced by:  nbbnOLD  387  pm5.17  1029  dn1  1073  sb8v  2385  sb8f  2386  dfeumo  2564  2ex2rexrot  3300  sbralie  3342  sbralieALT  3343  sbralieOLD  3344  ceqsralt  3489  reu8  3696  sbcimdv  3812  sbcg  3816  unass  4125  ssin  4191  difab  4263  csbab  4405  ralidm  4478  iunssf  5007  iunssfOLD  5008  iunss  5009  iunssOLD  5010  poirr  5581  elvvv  5737  cnvuni  5876  dfco2  6246  resin  6843  dffv2  6976  dff1o6  7273  fsplit  8108  naddasslem1  8677  naddasslem2  8678  sbthcl  9083  fiint  9282  rankf  9762  dfac3  10101  dfac5lem3  10105  elznn0  12601  elnn1uz2  12944  lsmspsn  21205  elold  28052  elzs2  28592  cmbr2i  31948  pjss2i  32032  iuninc  32905  fineqvrep  35527  dffr5  36246  brsset  36379  brtxpsd  36384  ellines  36644  axtco  36982  axtco1g  36987  mh-infprim2bi  37058  itg2addnclem3  38324  dvasin  38355  cvlsupr3  40118  dihglb2  42116  oneptri  43984  faosnf0.11b  44153  ifpidg  44217  dfsucon  44249  iscard4  44259  dffrege76  44665  dffrege99  44688  ntrneikb  44820  disjinfi  45910  2arwcatlem1  50373