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  2167  ssrab  3578  copsex2gb  5113  relop  5153  dmopab3  5215  issref  5380  fununi  5654  dffv2  5940  dfsup2  7902  kmlem3  8532  recmulnq  9342  ovoliunlem1  21676  shne0i  26070  ssiun3  27127  cnvoprab  27246  ind1a  27702  bnj1304  32975  bnj1253  33170  dalem20  34507