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  857  excxor  1423  sbequ8  1896  2sb5  2037  2sb6  2038  2sb5rf  2043  2sb6rf  2044  moabs  2130  moanim  2155  2eu4  2174  2eu7  2175  sb8ab  2356  risset  2570  cbvreuvw  2784  reuind  3022  difundi  3473  indifdir  3477  unab  3488  inab  3489  rabeq0  3538  abeq0  3539  inssdif0im  3576  snprc  3754  snssOLD  3819  unipr  3928  uni0b  3939  pwtr  4335  opm  4350  onintexmid  4695  elxp2  4767  opthprc  4801  xpiundir  4809  elvvv  4813  relun  4869  inopab  4887  difopab  4888  ralxpf  4901  rexxpf  4902  dmiun  4965  rniun  5173  cnvresima  5252  imaco  5268  fnopabg  5482  dff1o2  5619  idref  5929  imaiun  5933  opabex3d  6314  opabex3  6315  onntri35  7547  elixx3g  10234  elfz2  10349  elfzuzb  10353  divalgb  12611  1nprm  12811  issubg3  13909  cnfldui  14737  alsconv  16877