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  1515  ssrab  4036  copsex2gb  5769  relop  5814  dmopab3  5883  rnopab3  5920  dfres2  6012  restidsing  6024  fununi  6591  dffv2  6956  dfsup2  9395  kmlem3  10106  recmulnq  10917  dmscut  27723  nbgrel  29267  shne0i  31377  13an22anass  32393  ssiun3  32487  ind1a  32782  bnj1304  34809  bnj1253  35007  dfrecs2  35938  icorempo  37339  inxprnres  38280  disjressuc2  38374  dalem20  39687  ralopabb  43400  rp-isfinite6  43507  rababg  43563  nregmodel  45007  ssrabf  45108  ralfal  45155