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-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  dcnnOLD  817  excxor  1339  sbequ8  1801  2sb5  1934  2sb6  1935  2sb5rf  1940  2sb6rf  1941  moabs  2024  moanim  2049  2eu4  2068  2eu7  2069  sb8ab  2236  risset  2437  reuind  2858  difundi  3294  indifdir  3298  unab  3309  inab  3310  rabeq0  3358  abeq0  3359  inssdif0im  3396  snprc  3554  snss  3615  unipr  3716  uni0b  3727  pwtr  4101  opm  4116  onintexmid  4447  elxp2  4517  opthprc  4550  xpiundir  4558  elvvv  4562  relun  4616  inopab  4631  difopab  4632  ralxpf  4645  rexxpf  4646  dmiun  4708  rniun  4907  cnvresima  4986  imaco  5002  fnopabg  5204  dff1o2  5328  idref  5612  imaiun  5615  opabex3d  5973  opabex3  5974  elixx3g  9577  elfz2  9690  elfzuzb  9693  divalgb  11470  1nprm  11641  alsconv  12937