Theorem 3bitr2ri 197

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

Hypotheses

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

Assertion

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

Proof of Theorem 3bitr2ri

Step	Hyp	Ref	Expression
1		3bitr2i.1	. . 3 |- (ph <-> ps)
2		3bitr2i.2	. . 3 |- (ch <-> ps)
3	1, 2	bitr4i 193	. 2 |- (ph <-> ch)
4		3bitr2i.3	. 2 |- (ch <-> th)
5	3, 4	bitr2i 191	1 |- (th <-> ph)

Syntax hints:   <-> wb 163

This theorem is referenced by:  ssrab 2685  dfiin2g 3286  dfiin2OLD 3288  relop 4113  dmopab3 4169  ssrnres 4354  iunfopabOLD 4543  dffv2 4734  iinon 5115  uniqs 5354  kmlem3 5929  ltmullem 6824  sqr2irrlem4 7977  absgt0i 8094  cau3iri 8167  ntreq0 8984  shne0i 11004  chrelat2i 11937  bnj38 12409  bnj512 12519  bnj1222 12995  bnj611 13307  bnj965 13346  bnj1000 13364  dffr5 13831  dfiin2gOLD 15356  alexsublem3 15439  prter3 16286  pm13.196a 16378  hlrelat2 17052

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