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  3324  sbralieALT  3325  sbralieOLD  3326  ceqsralt  3477  reu8  3693  sbcimdv  3811  sbcg  3815  unass  4126  ssin  4193  difab  4264  csbab  4394  ralidm  4472  iunssf  5000  iunssfOLD  5001  iunss  5002  iunssOLD  5003  poirr  5552  elvvv  5708  cnvuni  5843  dfco2  6211  resin  6804  dffv2  6937  dff1o6  7231  fsplit  8069  naddasslem1  8632  naddasslem2  8633  sbthcl  9039  fiint  9239  rankf  9718  dfac3  10043  dfac5lem3  10047  elznn0  12515  elnn1uz2  12850  lsmspsn  21048  elold  27867  elzs2  28407  cmbr2i  31684  pjss2i  31768  iuninc  32647  fineqvrep  35292  dffr5  35970  brsset  36103  brtxpsd  36108  ellines  36368  itg2addnclem3  37924  dvasin  37955  cvlsupr3  39720  dihglb2  41718  oneptri  43614  faosnf0.11b  43783  ifpidg  43847  dfsucon  43879  iscard4  43889  dffrege76  44295  dffrege99  44318  ntrneikb  44450  disjinfi  45551  2arwcatlem1  49954