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  4359  opm  4374  onintexmid  4720  elxp2  4792  opthprc  4826  xpiundir  4834  elvvv  4838  relun  4894  inopab  4912  difopab  4913  ralxpf  4926  rexxpf  4927  dmiun  4990  rniun  5198  cnvresima  5277  imaco  5293  fnopabg  5507  dff1o2  5644  idref  5962  imaiun  5966  opabex3d  6350  opabex3  6351  onntri35  7596  elixx3g  10303  elfz2  10418  elfzuzb  10422  divalgb  12692  1nprm  12892  issubg3  13995  cnfldui  14924  stnot  17039