Theorem 3bitrri 301

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 279	. 2 ⊢ (𝜒 ↔ 𝜑)
5	1, 4	bitr3i 280	1 ⊢ (𝜃 ↔ 𝜑)

This proof depends on syntax axioms:   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  nbbnOLD  387  pm5.17  1029  dn1  1073  sb8v  2387  sb8f  2388  dfeumo  2566  2ex2rexrot  3302  sbralie  3344  sbralieALT  3345  sbralieOLD  3346  ceqsralt  3491  reu8  3698  sbcimdv  3814  sbcg  3818  unass  4125  ssin  4191  difab  4263  csbab  4405  ralidm  4480  iunssf  5009  iunssfOLD  5010  iunss  5011  iunssOLD  5012  poirr  5583  elvvv  5739  cnvuni  5878  dfco2  6248  resin  6847  dffv2  6980  dff1o6  7282  fsplit  8118  naddasslem1  8687  naddasslem2  8688  sbthcl  9094  fiint  9293  rankf  9773  dfac3  10121  dfac5lem3  10125  elznn0  12621  elnn1uz2  12965  lsmspsn  21255  elold  28103  elzs2  28643  cmbr2i  32019  pjss2i  32103  iuninc  32976  fineqvrep  35584  dffr5  36283  brsset  36416  brtxpsd  36421  ellines  36681  axtco  37039  axtco1g  37044  mh-infprim2bi  37115  itg2addnclem3  38381  dvasin  38412  cvlsupr3  40176  dihglb2  42174  oneptri  44042  faosnf0.11b  44211  ifpidg  44275  dfsucon  44307  iscard4  44317  dffrege76  44723  dffrege99  44746  ntrneikb  44878  disjinfi  45968  2arwcatlem1  50430