Theorem 3bitr2 179

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

Hypotheses

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

Assertion

Ref	Expression
3bitr2	|- (ph <-> th)

Proof of Theorem 3bitr2

Step	Hyp	Ref	Expression
1		3bitr2.1	. . 3 |- (ph <-> ps)
2		3bitr2.2	. . 3 |- (ch <-> ps)
3	1, 2	bitr4 176	. 2 |- (ph <-> ch)
4		3bitr2.3	. 2 |- (ch <-> th)
5	3, 4	bitr 173	1 |- (ph <-> th)

Syntax hints:   <-> wb 146

This theorem is referenced by:  pm5.17 670  2eu5 1456  2eu6 1457  exists1 1460  euxfr 1930  rmo4 1936  sspsstri 2151  symdif2 2269  ssiin 2603  dftr5 2688  pwundif 2834  uniuni 2886  reldm0 3337  imadisj 3428  eliniseg 3435  asymref2 3446  resco 3506  funcnv2 3562  funcnv3 3564  fncnv 3567  fun11 3568  fununi 3569  fsn 3840  fnoprval 4023  ixp0x 4365  mapsnen 4435  kmlem4 4778  kmlem12 4786  kmlem14 4788  kmlem15 4789  kmlem16 4790  ltexprlem4 5157  infcvglem1 7221  eirrlem1 7389  ruclem2 7512  istps3 7609  axgroth4 8775  grothprim 8778  pjtheu 9230  adjbd1o 10013

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