Theorem 3bitr2ri 274

Description: A chained inference from transitive law for logical equivalence. (Contributed by NM, 4-Aug-2006.)

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 252	. 2 |- ( ph <-> ch )
4		3bitr2i.3	. 2 |- ( ch <-> th )
5	3, 4	bitr2i 250	1 |- ( th <-> ph )

Syntax hints:   <-> wb 184

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 185

This theorem is referenced by:  sbnf2OLD  2153  ssrab  3533  copsex2gb  5053  relop  5093  dmopab3  5155  issref  5314  fununi  5587  dffv2  5868  dfsup2  7798  kmlem3  8427  recmulnq  9239  ovoliunlem1  21112  shne0i  24998  ssiun3  26055  cnvoprab  26169  ind1a  26617  bnj1304  32126  bnj1253  32321  dalem20  33656