Theorem 3bitr2ri 277

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

Syntax hints:   <-> wb 187

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 188

This theorem is referenced by:  xorass  1404  ssrab  3545  copsex2gb  4965  relop  5005  dmopab3  5067  issref  5233  fununi  5667  dffv2  5954  dfsup2  7964  kmlem3  8580  recmulnq  9388  ovoliunlem1  22333  shne0i  26936  ssiun3  28012  cnvoprab  28151  ind1a  28681  bnj1304  29419  bnj1253  29614  dfrecs2  30502  icorempt2  31488  dalem20  32967  rp-isfinite6  35862