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  845  excxor  1374  sbequ8  1841  2sb5  1977  2sb6  1978  2sb5rf  1983  2sb6rf  1984  moabs  2069  moanim  2094  2eu4  2113  2eu7  2114  sb8ab  2293  risset  2499  cbvreuvw  2703  reuind  2936  difundi  3380  indifdir  3384  unab  3395  inab  3396  rabeq0  3445  abeq0  3446  inssdif0im  3483  snprc  3649  snss  3710  unipr  3811  uni0b  3822  pwtr  4205  opm  4220  onintexmid  4558  elxp2  4630  opthprc  4663  xpiundir  4671  elvvv  4675  relun  4729  inopab  4744  difopab  4745  ralxpf  4758  rexxpf  4759  dmiun  4821  rniun  5023  cnvresima  5102  imaco  5118  fnopabg  5323  dff1o2  5450  idref  5740  imaiun  5743  opabex3d  6104  opabex3  6105  onntri35  7218  elixx3g  9862  elfz2  9976  elfzuzb  9979  divalgb  11888  1nprm  12072  alsconv  14194