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  851  excxor  1398  sbequ8  1870  2sb5  2011  2sb6  2012  2sb5rf  2017  2sb6rf  2018  moabs  2103  moanim  2128  2eu4  2147  2eu7  2148  sb8ab  2327  risset  2534  cbvreuvw  2744  reuind  2978  difundi  3425  indifdir  3429  unab  3440  inab  3441  rabeq0  3490  abeq0  3491  inssdif0im  3528  snprc  3698  snssOLD  3759  unipr  3864  uni0b  3875  pwtr  4263  opm  4278  onintexmid  4621  elxp2  4693  opthprc  4726  xpiundir  4734  elvvv  4738  relun  4792  inopab  4810  difopab  4811  ralxpf  4824  rexxpf  4825  dmiun  4887  rniun  5093  cnvresima  5172  imaco  5188  fnopabg  5399  dff1o2  5527  idref  5825  imaiun  5829  opabex3d  6206  opabex3  6207  onntri35  7349  elixx3g  10023  elfz2  10137  elfzuzb  10141  divalgb  12236  1nprm  12436  issubg3  13528  cnfldui  14351  alsconv  16019