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:  ssrab  3574  copsex2gb  5122  relop  5163  dmopab3  5225  issref  5390  fununi  5660  dffv2  5946  dfsup2  7920  kmlem3  8549  recmulnq  9359  ovoliunlem1  22038  shne0i  26492  ssiun3  27562  cnvoprab  27696  ind1a  28187  bnj1304  33979  bnj1253  34174  dalem20  35518  rp-isfinite6  37845