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  4376  uniuni  4599  rabxp  4814  eliunxp  4921  dmmrnm  5003  imadisj  5152  intirr  5177  resco  5295  funcnv3  5446  fncnv  5450  fun11  5451  fununi  5452  f1mpt  5980  mpomptx  6182  ixp0x  7012  mapsnen  7104  xpcomco  7128  enq0tr  7807  elq  10038  bitsmod  12748  pythagtrip  13091  ntreq0  15358  tx1cn  15495