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  2383  sb8f  2384  dfeumo  2562  2ex2rexrot  3298  sbralie  3339  sbralieALT  3340  sbralieOLD  3341  ceqsralt  3485  reu8  3691  sbcimdv  3807  sbcg  3811  unass  4118  ssin  4184  difab  4256  csbab  4398  ralidm  4473  iunssf  5001  iunssfOLD  5002  iunss  5003  iunssOLD  5004  eqvinot  5457  poirr  5571  elvvv  5727  cnvuni  5868  dfco2  6245  resin  6845  dffv2  6978  dff1o6  7281  fsplit  8126  naddasslem1  8697  naddasslem2  8698  sbthcl  9111  fiint  9311  rankf  9795  dfac3  10193  dfac5lem3  10197  elznn0  12701  elnn1uz2  13045  lsmspsn  21352  elold  28238  elzs2  28778  cmbr2i  32191  pjss2i  32275  iuninc  33148  fineqvrep  35765  dffr5  36498  brsset  36631  brtxpsd  36636  ellines  36897  axtco  37239  axtco1g  37244  mh-infprim2bi  37315  itg2addnclem3  38571  dvasin  38602  cvlsupr3  40381  dihglb2  42379  oneptri  44243  faosnf0.11b  44412  ifpidg  44476  dfsucon  44508  iscard4  44518  dffrege76  44924  dffrege99  44947  ntrneikb  45079  disjinfi  46176  2arwcatlem1  50672