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  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  3773  snssOLD  3838  unipr  3947  uni0b  3958  pwtr  4357  opm  4372  onintexmid  4718  elxp2  4790  opthprc  4824  xpiundir  4832  elvvv  4836  relun  4892  inopab  4910  difopab  4911  ralxpf  4924  rexxpf  4925  dmiun  4988  rniun  5196  cnvresima  5275  imaco  5291  fnopabg  5505  dff1o2  5642  idref  5956  imaiun  5960  opabex3d  6344  opabex3  6345  onntri35  7590  elixx3g  10286  elfz2  10401  elfzuzb  10405  divalgb  12675  1nprm  12875  issubg3  13978  cnfldui  14907