Theorem 3bitr4ri 202

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 176	. 2 |- ( ph <-> th )
5	1, 4	bitr2i 174	1 |- ( th <-> ch )

Syntax hints:   <-> wb 98

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  testbitestn  823  excxor  1269  sbequ8  1727  2sb5  1859  2sb6  1860  2sb5rf  1865  2sb6rf  1866  moabs  1949  moanim  1974  2eu4  1993  2eu7  1994  sb8ab  2159  risset  2352  reuind  2744  difundi  3189  indifdir  3193  unab  3204  inab  3205  rabeq0  3247  abeq0  3248  inssdif0im  3291  snprc  3435  snss  3494  unipr  3594  uni0b  3605  pwtr  3955  opm  3971  onintexmid  4297  elxp2  4363  opthprc  4391  xpiundir  4399  elvvv  4403  relun  4454  inopab  4468  difopab  4469  ralxpf  4482  rexxpf  4483  dmiun  4544  rniun  4734  cnvresima  4810  imaco  4826  fnopabg  5022  dff1o2  5131  idref  5396  imaiun  5399  opabex3d  5748  opabex3  5749  elixx3g  8770  elfz2  8881  elfzuzb  8884  alsconv  10119