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  2385  sb8f  2386  dfeumo  2564  2ex2rexrot  3301  sbralie  3342  sbralieALT  3343  sbralieOLD  3344  ceqsralt  3488  reu8  3694  sbcimdv  3810  sbcg  3814  ssin  4138  unass  4173  difab  4258  csbab  4401  ralidm  4476  iunssf  5006  iunssfOLD  5007  iunss  5008  iunssOLD  5009  eqvinot  5464  poirr  5578  elvvv  5735  cnvuni  5880  dfco2  6265  resin  6877  dffv2  7011  dff1o6  7314  fsplit  8165  naddasslem1  8742  naddasslem2  8743  sbthcl  9156  fiint  9356  rankf  9839  dfac3  10239  dfac5lem3  10243  elznn0  12748  elnn1uz2  13092  lsmspsn  21410  elold  28302  elzs2  28842  cmbr2i  32255  pjss2i  32339  iuninc  33253  fineqvrep  35923  dffr5  36734  brsset  36866  brtxpsd  36871  ellines  37132  axtco  37474  axtco1g  37479  mh-infprim2bi  37550  itg2addnclem3  38859  dvasin  38890  cvlsupr3  40667  dihglb2  42665  oneptri  44520  faosnf0.11b  44689  ifpidg  44753  dfsucon  44785  iscard4  44795  dffrege76  45200  dffrege99  45223  ntrneikb  45355  disjinfi  46480  2arwcatlem1  51064