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  1012  dn1  1058  sb8v  2358  sb8f  2359  dfeumo  2540  2ex2rexrot  3304  sbralie  3366  sbralieALT  3367  ceqsralt  3524  reu8  3755  sbcimdv  3878  sbcg  3883  unass  4195  ssin  4260  difab  4329  eq0rdv  4430  csbab  4463  ralidm  4535  iunssf  5067  iunss  5068  poirr  5620  elvvv  5775  cnvuni  5911  dfco2  6276  resin  6884  dffv2  7017  dff1o6  7311  fsplit  8158  naddasslem1  8750  naddasslem2  8751  sbthcl  9161  fiint  9394  fiintOLD  9395  rankf  9863  dfac3  10190  dfac5lem3  10194  elznn0  12654  elnn1uz2  12990  lsmspsn  21106  elold  27926  elzs2  28403  cmbr2i  31628  pjss2i  31712  iuninc  32583  fineqvrep  35071  dffr5  35716  brsset  35853  brtxpsd  35858  ellines  36116  itg2addnclem3  37633  dvasin  37664  cvlsupr3  39300  dihglb2  41299  oneptri  43218  faosnf0.11b  43389  ifpidg  43453  dfsucon  43485  iscard4  43495  dffrege76  43901  dffrege99  43924  ntrneikb  44056  disjinfi  45099