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  3793  unipr  3901  uni0b  3912  pwtr  4304  opm  4319  onintexmid  4662  elxp2  4734  opthprc  4767  xpiundir  4775  elvvv  4779  relun  4833  inopab  4851  difopab  4852  ralxpf  4865  rexxpf  4866  dmiun  4929  rniun  5135  cnvresima  5214  imaco  5230  fnopabg  5443  dff1o2  5573  idref  5873  imaiun  5877  opabex3d  6256  opabex3  6257  onntri35  7410  elixx3g  10085  elfz2  10199  elfzuzb  10203  divalgb  12422  1nprm  12622  issubg3  13715  cnfldui  14538  alsconv  16379