Theorem 3bitr2ri 289

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

Syntax hints:   <-> wb 196

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 197

This theorem is referenced by:  xorass  1468  ssrab  3680  copsex2gb  5230  relop  5272  dmopab3  5337  restidsing  5458  issref  5509  fununi  5964  dffv2  6271  dfsup2  8350  kmlem3  8974  recmulnq  9786  ovoliunlem1  23270  shne0i  28307  ssiun3  29376  cnvoprab  29498  ind1a  30081  bnj1304  30890  bnj1253  31085  dmscut  31918  dfrecs2  32057  icorempt2  33199  inxprnres  34060  dalem20  34979  rp-isfinite6  37864  rababg  37879  ssrabf  39298