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  1904  sbexyz  2022  exists1  2141  euxfrdc  2950  euind  2951  rmo4  2957  rmo3f  2961  rmo3  3081  ddifstab  3296  opm  4268  uniuni  4487  rabxp  4701  eliunxp  4806  dmmrnm  4886  imadisj  5032  intirr  5057  resco  5175  funcnv3  5321  fncnv  5325  fun11  5326  fununi  5327  f1mpt  5821  mpomptx  6017  ixp0x  6794  mapsnen  6879  xpcomco  6894  enq0tr  7518  elq  9713  bitsmod  12138  pythagtrip  12477  ntreq0  14452  tx1cn  14589