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 665  2eu5 1430  2eu6 1431  exists1 1434  euxfr 1898  rmo4 1904  sspsstri 2119  symdif2 2237  ssiin 2567  dftr5 2651  pwundif 2790  uniuni 2843  reldm0 3288  imadisj 3373  eliniseg 3380  resco 3442  funcnv2 3496  funcnv3 3498  fncnv 3501  fun11 3502  fununi 3503  fsn 3773  fnoprval 3956  ixp0x 4297  mapsnen 4364  kmlem4 4692  kmlem12 4700  kmlem14 4702  kmlem15 4703  kmlem16 4704  ltexprlem4 5068  infcvglem1 7107  eirrlem1 7281  ruclem2 7405  istps3 7501  axgroth4 8632  grothprim 8635  pjtheu 9364  adjbd1o 10147

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