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  849  excxor  1378  sbequ8  1847  2sb5  1983  2sb6  1984  2sb5rf  1989  2sb6rf  1990  moabs  2075  moanim  2100  2eu4  2119  2eu7  2120  sb8ab  2299  risset  2505  cbvreuvw  2709  reuind  2942  difundi  3387  indifdir  3391  unab  3402  inab  3403  rabeq0  3452  abeq0  3453  inssdif0im  3490  snprc  3657  snssOLD  3718  unipr  3823  uni0b  3834  pwtr  4219  opm  4234  onintexmid  4572  elxp2  4644  opthprc  4677  xpiundir  4685  elvvv  4689  relun  4743  inopab  4759  difopab  4760  ralxpf  4773  rexxpf  4774  dmiun  4836  rniun  5039  cnvresima  5118  imaco  5134  fnopabg  5339  dff1o2  5466  idref  5757  imaiun  5760  opabex3d  6121  opabex3  6122  onntri35  7235  elixx3g  9900  elfz2  10014  elfzuzb  10018  divalgb  11929  1nprm  12113  issubg3  13050  alsconv  14797