Theorem 3bitr2 179

Description: A chained inference from transitive law for logical equivalence.

Hypotheses

Ref	Expression
3bitr2.1	⊢ (φ ↔ ψ)
3bitr2.2	⊢ (χ ↔ ψ)
3bitr2.3	⊢ (χ ↔ θ)

Assertion

Ref	Expression
3bitr2	⊢ (φ ↔ θ)

Proof of Theorem 3bitr2

Step	Hyp	Ref	Expression
1		3bitr2.1	. . 3 ⊢ (φ ↔ ψ)
2		3bitr2.2	. . 3 ⊢ (χ ↔ ψ)
3	1, 2	bitr4 176	. 2 ⊢ (φ ↔ χ)
4		3bitr2.3	. 2 ⊢ (χ ↔ θ)
5	3, 4	bitr 173	1 ⊢ (φ ↔ θ)

Syntax hints:   ↔ wb 146

This theorem is referenced by:  pm5.17 667  2eu5 1451  2eu6 1452  exists1 1455  euxfr 1923  rmo4 1929  sspsstri 2144  symdif2 2262  ssiin 2594  dftr5 2678  pwundif 2823  uniuni 2875  reldm0 3326  imadisj 3414  eliniseg 3421  asymref2 3432  resco 3492  funcnv2 3548  funcnv3 3550  fncnv 3553  fun11 3554  fununi 3555  fsn 3825  fnoprval 4008  ixp0x 4349  mapsnen 4416  kmlem4 4748  kmlem12 4756  kmlem14 4758  kmlem15 4759  kmlem16 4760  ltexprlem4 5125  infcvglem1 7164  eirrlem1 7338  ruclem2 7462  istps3 7558  axgroth4 8719  grothprim 8722  pjtheu 9173  adjbd1o 9956

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 147

Copyright terms: Public domain