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  3690  sbcimdv  3806  sbcg  3810  ssin  4134  unass  4169  difab  4254  csbab  4397  ralidm  4472  iunssf  5000  iunssfOLD  5001  iunss  5002  iunssOLD  5003  eqvinot  5457  poirr  5571  elvvv  5728  cnvuni  5869  dfco2  6249  resin  6852  dffv2  6985  dff1o6  7287  fsplit  8134  naddasslem1  8711  naddasslem2  8712  sbthcl  9125  fiint  9325  rankf  9809  dfac3  10207  dfac5lem3  10211  elznn0  12715  elnn1uz2  13059  lsmspsn  21368  elold  28254  elzs2  28794  cmbr2i  32207  pjss2i  32291  iuninc  33206  fineqvrep  35842  dffr5  36615  brsset  36747  brtxpsd  36752  ellines  37013  axtco  37355  axtco1g  37360  mh-infprim2bi  37431  itg2addnclem3  38700  dvasin  38731  cvlsupr3  40510  dihglb2  42508  oneptri  44368  faosnf0.11b  44537  ifpidg  44601  dfsucon  44633  iscard4  44643  dffrege76  45048  dffrege99  45071  ntrneikb  45203  disjinfi  46315  2arwcatlem1  50841