Theorem 3bitrri 297

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

Syntax hints:   ↔ wb 205

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 206

This theorem is referenced by:  nbbn  384  pm5.17  1010  dn1  1056  sb8v  2348  sb8f  2349  dfeumo  2531  2ex2rexrot  3295  sbralie  3354  sbralieALT  3355  ceqsralt  3506  reu8  3729  sbcimdv  3851  sbcg  3856  unass  4166  ssin  4230  difab  4300  eq0rdv  4404  csbab  4437  ralidm  4511  iunssf  5047  iunss  5048  poirr  5600  elvvv  5751  cnvuni  5886  dfco2  6244  resin  6855  dffv2  6986  dff1o6  7272  fsplit  8102  naddasslem1  8692  naddasslem2  8693  sbthcl  9094  fiint  9323  rankf  9788  dfac3  10115  dfac5lem3  10119  elznn0  12572  elnn1uz2  12908  lsmspsn  20694  elold  27361  cmbr2i  30844  pjss2i  30928  iuninc  31787  fineqvrep  34090  dffr5  34719  brsset  34856  brtxpsd  34861  ellines  35119  itg2addnclem3  36536  dvasin  36567  cvlsupr3  38209  dihglb2  40208  oneptri  41996  faosnf0.11b  42168  ifpidg  42232  dfsucon  42264  iscard4  42274  dffrege76  42680  dffrege99  42703  ntrneikb  42835  disjinfi  43881