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 668  2eu5 1453  2eu6 1454  exists1 1457  euxfr 1927  rmo4 1933  sspsstri 2148  symdif2 2266  ssiin 2599  dftr5 2683  pwundif 2828  uniuni 2880  reldm0 3331  imadisj 3422  eliniseg 3429  asymref2 3440  resco 3500  funcnv2 3556  funcnv3 3558  fncnv 3561  fun11 3562  fununi 3563  fsn 3834  fnoprval 4017  ixp0x 4359  mapsnen 4429  kmlem4 4768  kmlem12 4776  kmlem14 4778  kmlem15 4779  kmlem16 4780  ltexprlem4 5145  infcvglem1 7221  eirrlem1 7389  ruclem2 7511  istps3 7608  axgroth4 8780  grothprim 8783  pjtheu 9235  adjbd1o 10018

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