Theorem 3bitr2i 207

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

Syntax hints:   <-> wb 104

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  an13  552  sbanv  1861  sbexyz  1978  exists1  2095  euxfrdc  2870  euind  2871  rmo4  2877  rmo3f  2881  rmo3  3000  ddifstab  3208  opm  4156  uniuni  4372  rabxp  4576  eliunxp  4678  dmmrnm  4758  imadisj  4901  intirr  4925  resco  5043  funcnv3  5185  fncnv  5189  fun11  5190  fununi  5191  f1mpt  5672  mpomptx  5862  ixp0x  6620  mapsnen  6705  xpcomco  6720  enq0tr  7242  elq  9414  ntreq0  12301  tx1cn  12438