Theorem 3bitr2ri 278

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

Syntax hints:   <-> wb 188

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 189

This theorem is referenced by:  xorass  1408  ssrab  3506  copsex2gb  4944  relop  4984  dmopab3  5046  issref  5212  fununi  5647  dffv2  5936  dfsup2  7955  kmlem3  8579  recmulnq  9386  ovoliunlem1  22448  shne0i  27094  ssiun3  28166  cnvoprab  28301  ind1a  28835  bnj1304  29624  bnj1253  29819  dfrecs2  30710  icorempt2  31747  dalem20  33252  rp-isfinite6  36157  rababg  36173