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  1901  sbexyz  2019  exists1  2138  euxfrdc  2946  euind  2947  rmo4  2953  rmo3f  2957  rmo3  3077  ddifstab  3291  opm  4263  uniuni  4482  rabxp  4696  eliunxp  4801  dmmrnm  4881  imadisj  5027  intirr  5052  resco  5170  funcnv3  5316  fncnv  5320  fun11  5321  fununi  5322  f1mpt  5814  mpomptx  6009  ixp0x  6780  mapsnen  6865  xpcomco  6880  enq0tr  7494  elq  9687  pythagtrip  12421  ntreq0  14300  tx1cn  14437