Theorem 3bitr2ri 300

Description: A chained inference from transitive law for logical equivalence. (Contributed by NM, 4-Aug-2006.)

Hypotheses

Ref	Expression
3bitr2i.1	⊢ (𝜑 ↔ 𝜓)
3bitr2i.2	⊢ (𝜒 ↔ 𝜓)
3bitr2i.3	⊢ (𝜒 ↔ 𝜃)

Assertion

Ref	Expression
3bitr2ri	⊢ (𝜃 ↔ 𝜑)

Proof of Theorem 3bitr2ri

Step	Hyp	Ref	Expression
1		3bitr2i.1	. . 3 ⊢ (𝜑 ↔ 𝜓)
2		3bitr2i.2	. . 3 ⊢ (𝜒 ↔ 𝜓)
3	1, 2	bitr4i 278	. 2 ⊢ (𝜑 ↔ 𝜒)
4		3bitr2i.3	. 2 ⊢ (𝜒 ↔ 𝜃)
5	3, 4	bitr2i 276	1 ⊢ (𝜃 ↔ 𝜑)

Syntax hints:   ↔ wb 206

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 207

This theorem is referenced by:  xorass  1516  ssrab  4020  copsex2gb  5750  relop  5794  dmopab3  5863  rnopab3  5900  dfres2  5994  restidsing  6006  fununi  6561  dffv2  6923  dfsup2  9335  kmlem3  10051  recmulnq  10862  dmscut  27753  nbgrel  29320  shne0i  31430  13an22anass  32445  ssiun3  32540  ind1a  32845  bnj1304  34852  bnj1253  35050  dfrecs2  36015  icorempo  37416  inxprnres  38351  disjressuc2  38456  dalem20  39813  ralopabb  43529  rp-isfinite6  43636  rababg  43692  nregmodel  45135  ssrabf  45236  ralfal  45283