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  2382  sb8f  2383  dfeumo  2561  2ex2rexrot  3297  sbralie  3338  sbralieALT  3339  sbralieOLD  3340  ceqsralt  3484  reu8  3691  sbcimdv  3807  sbcg  3811  unass  4118  ssin  4184  difab  4256  csbab  4398  ralidm  4473  iunssf  5001  iunssfOLD  5002  iunss  5003  iunssOLD  5004  poirr  5575  elvvv  5731  cnvuni  5870  dfco2  6241  resin  6840  dffv2  6973  dff1o6  7276  fsplit  8114  naddasslem1  8683  naddasslem2  8684  sbthcl  9097  fiint  9296  rankf  9776  dfac3  10124  dfac5lem3  10128  elznn0  12630  elnn1uz2  12974  lsmspsn  21268  elold  28124  elzs2  28664  cmbr2i  32077  pjss2i  32161  iuninc  33034  fineqvrep  35640  dffr5  36333  brsset  36466  brtxpsd  36471  ellines  36732  axtco  37090  axtco1g  37095  mh-infprim2bi  37166  itg2addnclem3  38422  dvasin  38453  cvlsupr3  40217  dihglb2  42215  oneptri  44098  faosnf0.11b  44267  ifpidg  44331  dfsucon  44363  iscard4  44373  dffrege76  44779  dffrege99  44802  ntrneikb  44934  disjinfi  46024  2arwcatlem1  50521