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  565  sbanv  1939  sbexyz  2057  exists1  2177  euxfrdc  3003  euind  3004  rmo4  3010  rmo3f  3014  rmo3  3135  ddifstab  3351  opm  4350  uniuni  4572  rabxp  4787  eliunxp  4894  dmmrnm  4976  imadisj  5124  intirr  5149  resco  5267  funcnv3  5418  fncnv  5422  fun11  5423  fununi  5424  f1mpt  5944  mpomptx  6144  ixp0x  6961  mapsnen  7053  xpcomco  7077  enq0tr  7749  elq  9954  bitsmod  12642  pythagtrip  12981  ntreq0  14997  tx1cn  15134