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 )

This proof depends on syntax axioms:   <-> wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  an13  569  sbanv  1944  sbexyz  2063  exists1  2183  euxfrdc  3012  euind  3013  rmo4  3019  rmo3f  3023  rmo3  3144  ddifstab  3361  opm  4374  uniuni  4597  rabxp  4812  eliunxp  4919  dmmrnm  5001  imadisj  5149  intirr  5174  resco  5292  funcnv3  5443  fncnv  5447  fun11  5448  fununi  5449  f1mpt  5977  mpomptx  6179  ixp0x  7008  mapsnen  7100  xpcomco  7124  enq0tr  7801  elq  10022  bitsmod  12723  pythagtrip  13062  ntreq0  15233  tx1cn  15370