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 )

This proof depends on syntax axioms:   <-> wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  dcnnOLD  861  excxor  1427  sbequ8  1900  2sb5  2043  2sb6  2044  2sb5rf  2049  2sb6rf  2050  moabs  2136  moanim  2161  2eu4  2180  2eu7  2181  sb8ab  2362  risset  2578  cbvreuvw  2792  reuind  3031  difundi  3483  indifdir  3487  unab  3498  inab  3499  rabeq0  3552  abeq0  3553  inssdif0imOLD  3593  snprc  3774  snssOLD  3840  unipr  3949  uni0b  3960  pwtr  4361  opm  4376  onintexmid  4722  elxp2  4794  opthprc  4828  xpiundir  4836  elvvv  4840  relun  4896  inopab  4914  difopab  4915  ralxpf  4928  rexxpf  4929  dmiun  4992  rniun  5201  cnvresima  5280  imaco  5296  fnopabg  5510  dff1o2  5647  idref  5965  imaiun  5969  opabex3d  6354  opabex3  6355  onntri35  7602  elixx3g  10320  elfz2  10435  elfzuzb  10439  divalgb  12717  1nprm  12917  issubg3  14054  cnfldui  15033  stnot  17244