Theorem 3bitr2i 208

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
3bitr2i	|- ( ph <-> th )

Proof of Theorem 3bitr2i

Step	Hyp	Ref	Expression
1		3bitr2i.1	. . 3 |- ( ph <-> ps )
2		3bitr2i.2	. . 3 |- ( ch <-> ps )
3	1, 2	bitr4i 187	. 2 |- ( ph <-> ch )
4		3bitr2i.3	. 2 |- ( ch <-> th )
5	3, 4	bitri 184	1 |- ( ph <-> th )

Syntax hints:   <-> wb 105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  an13  563  sbanv  1936  sbexyz  2054  exists1  2174  euxfrdc  2990  euind  2991  rmo4  2997  rmo3f  3001  rmo3  3122  ddifstab  3337  opm  4324  uniuni  4546  rabxp  4761  eliunxp  4867  dmmrnm  4949  imadisj  5096  intirr  5121  resco  5239  funcnv3  5389  fncnv  5393  fun11  5394  fununi  5395  f1mpt  5907  mpomptx  6107  ixp0x  6890  mapsnen  6981  xpcomco  7005  enq0tr  7644  elq  9846  bitsmod  12507  pythagtrip  12846  ntreq0  14846  tx1cn  14983