Theorem 3bitr4ri 212

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

Syntax hints:   <-> wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  dcnnOLD  835  excxor  1357  sbequ8  1820  2sb5  1959  2sb6  1960  2sb5rf  1965  2sb6rf  1966  moabs  2049  moanim  2074  2eu4  2093  2eu7  2094  sb8ab  2262  risset  2466  reuind  2893  difundi  3333  indifdir  3337  unab  3348  inab  3349  rabeq0  3397  abeq0  3398  inssdif0im  3435  snprc  3596  snss  3657  unipr  3758  uni0b  3769  pwtr  4149  opm  4164  onintexmid  4495  elxp2  4565  opthprc  4598  xpiundir  4606  elvvv  4610  relun  4664  inopab  4679  difopab  4680  ralxpf  4693  rexxpf  4694  dmiun  4756  rniun  4957  cnvresima  5036  imaco  5052  fnopabg  5254  dff1o2  5380  idref  5666  imaiun  5669  opabex3d  6027  opabex3  6028  elixx3g  9714  elfz2  9828  elfzuzb  9831  divalgb  11658  1nprm  11831  alsconv  13437