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  2351  sb8f  2352  dfeumo  2530  2ex2rexrot  3271  sbralie  3323  sbralieALT  3324  sbralieOLD  3325  ceqsralt  3479  reu8  3701  sbcimdv  3819  sbcg  3823  unass  4131  ssin  4198  difab  4269  eq0rdv  4366  csbab  4399  ralidm  4471  iunssf  5003  iunss  5004  poirr  5551  elvvv  5707  cnvuni  5840  dfco2  6206  resin  6804  dffv2  6938  dff1o6  7232  fsplit  8073  naddasslem1  8635  naddasslem2  8636  sbthcl  9040  fiint  9253  fiintOLD  9254  rankf  9723  dfac3  10050  dfac5lem3  10054  elznn0  12520  elnn1uz2  12860  lsmspsn  20967  elold  27757  elzs2  28263  cmbr2i  31498  pjss2i  31582  iuninc  32462  fineqvrep  35058  dffr5  35714  brsset  35850  brtxpsd  35855  ellines  36113  itg2addnclem3  37640  dvasin  37671  cvlsupr3  39310  dihglb2  41309  oneptri  43219  faosnf0.11b  43389  ifpidg  43453  dfsucon  43485  iscard4  43495  dffrege76  43901  dffrege99  43924  ntrneikb  44056  disjinfi  45159  2arwcatlem1  49557