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  854  excxor  1420  sbequ8  1893  2sb5  2034  2sb6  2035  2sb5rf  2040  2sb6rf  2041  moabs  2127  moanim  2152  2eu4  2171  2eu7  2172  sb8ab  2351  risset  2558  cbvreuvw  2771  reuind  3008  difundi  3456  indifdir  3460  unab  3471  inab  3472  rabeq0  3521  abeq0  3522  inssdif0im  3559  snprc  3731  snssOLD  3794  unipr  3902  uni0b  3913  pwtr  4305  opm  4320  onintexmid  4665  elxp2  4737  opthprc  4770  xpiundir  4778  elvvv  4782  relun  4836  inopab  4854  difopab  4855  ralxpf  4868  rexxpf  4869  dmiun  4932  rniun  5139  cnvresima  5218  imaco  5234  fnopabg  5447  dff1o2  5579  idref  5886  imaiun  5890  opabex3d  6272  opabex3  6273  onntri35  7430  elixx3g  10105  elfz2  10219  elfzuzb  10223  divalgb  12444  1nprm  12644  issubg3  13737  cnfldui  14561  alsconv  16478