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  839  excxor  1368  sbequ8  1835  2sb5  1971  2sb6  1972  2sb5rf  1977  2sb6rf  1978  moabs  2063  moanim  2088  2eu4  2107  2eu7  2108  sb8ab  2288  risset  2494  cbvreuvw  2698  reuind  2931  difundi  3374  indifdir  3378  unab  3389  inab  3390  rabeq0  3438  abeq0  3439  inssdif0im  3476  snprc  3641  snss  3702  unipr  3803  uni0b  3814  pwtr  4197  opm  4212  onintexmid  4550  elxp2  4622  opthprc  4655  xpiundir  4663  elvvv  4667  relun  4721  inopab  4736  difopab  4737  ralxpf  4750  rexxpf  4751  dmiun  4813  rniun  5014  cnvresima  5093  imaco  5109  fnopabg  5311  dff1o2  5437  idref  5725  imaiun  5728  opabex3d  6089  opabex3  6090  onntri35  7193  elixx3g  9837  elfz2  9951  elfzuzb  9954  divalgb  11862  1nprm  12046  alsconv  13956