Theorem 3bitr3ri 199

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

Hypotheses

Ref	Expression
3bitr3i.1	|- (ph <-> ps)
3bitr3i.2	|- (ph <-> ch)
3bitr3i.3	|- (ps <-> th)

Assertion

Ref	Expression
3bitr3ri	|- (th <-> ch)

Proof of Theorem 3bitr3ri

Step	Hyp	Ref	Expression
1		3bitr3i.3	. 2 |- (ps <-> th)
2		3bitr3i.1	. . 3 |- (ph <-> ps)
3		3bitr3i.2	. . 3 |- (ph <-> ch)
4	2, 3	bitr3i 192	. 2 |- (ps <-> ch)
5	1, 4	bitr3i 192	1 |- (th <-> ch)

Syntax hints:   <-> wb 163

This theorem is referenced by:  bigolden 819  2eu6 1858  2eu8 1860  ralcom4OLD 2311  rexcom4OLD 2313  sbc2ie 2523  sbc2iedv 2524  zfpair 3522  opabidOLD 3558  intirrOLD 4313  dmsnn0OLD 4363  dffun6f 4435  fununi 4481  tfrlem2 5120  sbthcl 5522  xpmapenlem4 5593  abfii2 5652  kmlem3 5929  lesub0iOLD 6793  sqeqori 7893  bcpasci 8221  tgss3 8908  nmcopexlem1 11588  nmcfnexlem1 11617  isprm2lem 13774  axfelem15 14045  firnfi3 15743

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 164

Copyright terms: Public domain