Theorem 3bitr4ri 213

Description: A chained inference from transitive law for logical equivalence. (Contributed by NM, 2-Sep-1995.)

Hypotheses

Ref	Expression
3bitr4i.1	⊢ (𝜑 ↔ 𝜓)
3bitr4i.2	⊢ (𝜒 ↔ 𝜑)
3bitr4i.3	⊢ (𝜃 ↔ 𝜓)

Assertion

Ref	Expression
3bitr4ri	⊢ (𝜃 ↔ 𝜒)

Proof of Theorem 3bitr4ri

Step	Hyp	Ref	Expression
1		3bitr4i.2	. 2 ⊢ (𝜒 ↔ 𝜑)
2		3bitr4i.1	. . 3 ⊢ (𝜑 ↔ 𝜓)
3		3bitr4i.3	. . 3 ⊢ (𝜃 ↔ 𝜓)
4	2, 3	bitr4i 187	. 2 ⊢ (𝜑 ↔ 𝜃)
5	1, 4	bitr2i 185	1 ⊢ (𝜃 ↔ 𝜒)

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  2783  reuind  3021  difundi  3472  indifdir  3476  unab  3487  inab  3488  rabeq0  3537  abeq0  3538  inssdif0im  3575  snprc  3753  snssOLD  3818  unipr  3927  uni0b  3938  pwtr  4334  opm  4349  onintexmid  4694  elxp2  4766  opthprc  4800  xpiundir  4808  elvvv  4812  relun  4868  inopab  4886  difopab  4887  ralxpf  4900  rexxpf  4901  dmiun  4964  rniun  5172  cnvresima  5251  imaco  5267  fnopabg  5481  dff1o2  5618  idref  5928  imaiun  5932  opabex3d  6313  opabex3  6314  onntri35  7546  elixx3g  10233  elfz2  10348  elfzuzb  10352  divalgb  12607  1nprm  12807  issubg3  13901  cnfldui  14729  alsconv  16868