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 ⊢ (𝜃 ↔ 𝜒)

This proof depends on syntax axioms:   ↔ wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used 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  3774  snssOLD  3840  unipr  3949  uni0b  3960  pwtr  4359  opm  4374  onintexmid  4720  elxp2  4792  opthprc  4826  xpiundir  4834  elvvv  4838  relun  4894  inopab  4912  difopab  4913  ralxpf  4926  rexxpf  4927  dmiun  4990  rniun  5198  cnvresima  5277  imaco  5293  fnopabg  5507  dff1o2  5644  idref  5962  imaiun  5966  opabex3d  6350  opabex3  6351  onntri35  7596  elixx3g  10305  elfz2  10420  elfzuzb  10424  divalgb  12694  1nprm  12894  issubg3  13997  cnfldui  14926  stnot  17051