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  1027  dn1  1071  sb8v  2391  sb8f  2392  dfeumo  2570  2ex2rexrot  3306  sbralie  3349  sbralieALT  3350  sbralieOLD  3351  ceqsralt  3497  reu8  3705  sbcimdv  3821  sbcg  3825  unass  4133  ssin  4199  difab  4271  csbab  4411  ralidm  4483  iunssf  5011  iunssfOLD  5012  iunss  5013  iunssOLD  5014  poirr  5582  elvvv  5738  cnvuni  5877  dfco2  6247  resin  6844  dffv2  6977  dff1o6  7274  fsplit  8111  naddasslem1  8680  naddasslem2  8681  sbthcl  9086  fiint  9285  rankf  9765  dfac3  10104  dfac5lem3  10108  elznn0  12605  elnn1uz2  12948  lsmspsn  21182  elold  28017  elzs2  28557  cmbr2i  31888  pjss2i  31972  iuninc  32845  fineqvrep  35449  dffr5  36144  brsset  36277  brtxpsd  36282  ellines  36542  axtco  36870  axtco1g  36875  mh-infprim2bi  36946  itg2addnclem3  38211  dvasin  38242  cvlsupr3  40007  dihglb2  42005  oneptri  43875  faosnf0.11b  44044  ifpidg  44108  dfsucon  44140  iscard4  44150  dffrege76  44556  dffrege99  44579  ntrneikb  44711  disjinfi  45801  2arwcatlem1  50257