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 205

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 206

This theorem is referenced by:  nbbn  383  pm5.17  1009  dn1  1055  sb8v  2347  sb8f  2348  dfeumo  2530  2ex2rexrot  3294  sbralie  3353  sbralieALT  3354  ceqsralt  3506  reu8  3729  sbcimdv  3851  sbcg  3856  unass  4166  ssin  4230  difab  4300  eq0rdv  4404  csbab  4437  ralidm  4511  iunssf  5047  iunss  5048  poirr  5600  elvvv  5751  cnvuni  5886  dfco2  6244  resin  6855  dffv2  6986  dff1o6  7276  fsplit  8106  naddasslem1  8696  naddasslem2  8697  sbthcl  9098  fiint  9327  rankf  9792  dfac3  10119  dfac5lem3  10123  elznn0  12578  elnn1uz2  12914  lsmspsn  20840  elold  27602  cmbr2i  31117  pjss2i  31201  iuninc  32060  fineqvrep  34394  dffr5  35029  brsset  35166  brtxpsd  35171  ellines  35429  itg2addnclem3  36845  dvasin  36876  cvlsupr3  38518  dihglb2  40517  oneptri  42309  faosnf0.11b  42481  ifpidg  42545  dfsucon  42577  iscard4  42587  dffrege76  42993  dffrege99  43016  ntrneikb  43148  disjinfi  44190