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  2947  euind  2948  rmo4  2954  rmo3f  2958  rmo3  3078  ddifstab  3292  opm  4264  uniuni  4483  rabxp  4697  eliunxp  4802  dmmrnm  4882  imadisj  5028  intirr  5053  resco  5171  funcnv3  5317  fncnv  5321  fun11  5322  fununi  5323  f1mpt  5815  mpomptx  6010  ixp0x  6782  mapsnen  6867  xpcomco  6882  enq0tr  7496  elq  9690  pythagtrip  12424  ntreq0  14311  tx1cn  14448