Theorem 3bitr2ri 282

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

Syntax hints:   <-> wb 189

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 190

This theorem is referenced by:  xorass  1434  ssrab  3493  copsex2gb  4950  relop  4990  dmopab3  5053  issref  5219  fununi  5659  dffv2  5953  dfsup2  7976  kmlem3  8600  recmulnq  9407  ovoliunlem1  22533  shne0i  27182  ssiun3  28251  cnvoprab  28383  ind1a  28916  bnj1304  29703  bnj1253  29898  dfrecs2  30788  icorempt2  31824  dalem20  33329  rp-isfinite6  36234  rababg  36250