Theorem 3bitr4ri 212

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 186	. 2 ⊢ (𝜑 ↔ 𝜃)
5	1, 4	bitr2i 184	1 ⊢ (𝜃 ↔ 𝜒)

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  834  excxor  1356  sbequ8  1819  2sb5  1956  2sb6  1957  2sb5rf  1962  2sb6rf  1963  moabs  2046  moanim  2071  2eu4  2090  2eu7  2091  sb8ab  2259  risset  2461  reuind  2884  difundi  3323  indifdir  3327  unab  3338  inab  3339  rabeq0  3387  abeq0  3388  inssdif0im  3425  snprc  3583  snss  3644  unipr  3745  uni0b  3756  pwtr  4136  opm  4151  onintexmid  4482  elxp2  4552  opthprc  4585  xpiundir  4593  elvvv  4597  relun  4651  inopab  4666  difopab  4667  ralxpf  4680  rexxpf  4681  dmiun  4743  rniun  4944  cnvresima  5023  imaco  5039  fnopabg  5241  dff1o2  5365  idref  5651  imaiun  5654  opabex3d  6012  opabex3  6013  elixx3g  9677  elfz2  9790  elfzuzb  9793  divalgb  11611  1nprm  11784  alsconv  13235