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  1013  dn1  1057  sb8v  2354  sb8f  2355  dfeumo  2536  2ex2rexrot  3297  sbralie  3357  sbralieALT  3358  ceqsralt  3515  reu8  3738  sbcimdv  3858  sbcg  3862  unass  4171  ssin  4238  difab  4309  eq0rdv  4406  csbab  4439  ralidm  4511  iunssf  5043  iunss  5044  poirr  5603  elvvv  5760  cnvuni  5896  dfco2  6264  resin  6869  dffv2  7003  dff1o6  7296  fsplit  8143  naddasslem1  8733  naddasslem2  8734  sbthcl  9136  fiint  9367  fiintOLD  9368  rankf  9835  dfac3  10162  dfac5lem3  10166  elznn0  12630  elnn1uz2  12968  lsmspsn  21084  elold  27909  elzs2  28386  cmbr2i  31616  pjss2i  31700  iuninc  32574  fineqvrep  35110  dffr5  35755  brsset  35891  brtxpsd  35896  ellines  36154  itg2addnclem3  37681  dvasin  37712  cvlsupr3  39346  dihglb2  41345  oneptri  43274  faosnf0.11b  43445  ifpidg  43509  dfsucon  43541  iscard4  43551  dffrege76  43957  dffrege99  43980  ntrneikb  44112  disjinfi  45202