Theorem 3bitr4ri 213

Description: A chained inference from transitive law for logical equivalence. (Contributed by NM, 2-Sep-1995.)

Hypotheses

Ref	Expression
3bitr4i.1	|- ( ph <-> ps )
3bitr4i.2	|- ( ch <-> ph )
3bitr4i.3	|- ( th <-> ps )

Assertion

Ref	Expression
3bitr4ri	|- ( th <-> ch )

Proof of Theorem 3bitr4ri

Step	Hyp	Ref	Expression
1		3bitr4i.2	. 2 |- ( ch <-> ph )
2		3bitr4i.1	. . 3 |- ( ph <-> ps )
3		3bitr4i.3	. . 3 |- ( th <-> ps )
4	2, 3	bitr4i 187	. 2 |- ( ph <-> th )
5	1, 4	bitr2i 185	1 |- ( th <-> ch )

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:  dcnnOLD  850  excxor  1389  sbequ8  1858  2sb5  1999  2sb6  2000  2sb5rf  2005  2sb6rf  2006  moabs  2091  moanim  2116  2eu4  2135  2eu7  2136  sb8ab  2315  risset  2522  cbvreuvw  2732  reuind  2966  difundi  3412  indifdir  3416  unab  3427  inab  3428  rabeq0  3477  abeq0  3478  inssdif0im  3515  snprc  3684  snssOLD  3745  unipr  3850  uni0b  3861  pwtr  4249  opm  4264  onintexmid  4606  elxp2  4678  opthprc  4711  xpiundir  4719  elvvv  4723  relun  4777  inopab  4795  difopab  4796  ralxpf  4809  rexxpf  4810  dmiun  4872  rniun  5077  cnvresima  5156  imaco  5172  fnopabg  5378  dff1o2  5506  idref  5800  imaiun  5804  opabex3d  6175  opabex3  6176  onntri35  7299  elixx3g  9970  elfz2  10084  elfzuzb  10088  divalgb  12069  1nprm  12255  issubg3  13265  cnfldui  14088  alsconv  15640