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 666  2eu5 1446  2eu6 1447  exists1 1450  euxfr 1917  rmo4 1923  sspsstri 2138  symdif2 2256  ssiin 2589  dftr5 2673  pwundif 2817  uniuni 2870  reldm0 3320  imadisj 3406  eliniseg 3413  asymref2 3424  asymref2OLD 3426  resco 3486  funcnv2 3542  funcnv3 3544  fncnv 3547  fun11 3548  fununi 3549  fsn 3819  fnoprval 4002  ixp0x 4343  mapsnen 4410  kmlem4 4740  kmlem12 4748  kmlem14 4750  kmlem15 4751  kmlem16 4752  ltexprlem4 5117  infcvglem1 7156  eirrlem1 7330  ruclem2 7454  istps3 7550  axgroth4 8719  grothprim 8722  pjtheu 9150  adjbd1o 9933

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