Theorem 3bitr4ri 211

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

Syntax hints:   <-> wb 103

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

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  testbitestn  856  excxor  1309  sbequ8  1768  2sb5  1900  2sb6  1901  2sb5rf  1906  2sb6rf  1907  moabs  1990  moanim  2015  2eu4  2034  2eu7  2035  sb8ab  2200  risset  2394  reuind  2795  difundi  3216  indifdir  3220  unab  3231  inab  3232  rabeq0  3274  abeq0  3275  inssdif0im  3311  snprc  3457  snss  3516  unipr  3615  uni0b  3626  pwtr  3974  opm  3989  onintexmid  4315  elxp2  4381  opthprc  4409  xpiundir  4417  elvvv  4421  relun  4472  inopab  4486  difopab  4487  ralxpf  4500  rexxpf  4501  dmiun  4562  rniun  4754  cnvresima  4830  imaco  4846  fnopabg  5042  dff1o2  5151  idref  5417  imaiun  5420  opabex3d  5768  opabex3  5769  elixx3g  8924  elfz2  9036  elfzuzb  9039  divalgb  10325  1nprm  10496  alsconv  10791