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  1913  sbexyz  2031  exists1  2150  euxfrdc  2959  euind  2960  rmo4  2966  rmo3f  2970  rmo3  3090  ddifstab  3305  opm  4278  uniuni  4498  rabxp  4712  eliunxp  4817  dmmrnm  4897  imadisj  5044  intirr  5069  resco  5187  funcnv3  5336  fncnv  5340  fun11  5341  fununi  5342  f1mpt  5840  mpomptx  6036  ixp0x  6813  mapsnen  6903  xpcomco  6921  enq0tr  7547  elq  9743  bitsmod  12267  pythagtrip  12606  ntreq0  14604  tx1cn  14741