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  1517  ssrab  4025  copsex2gb  5763  relop  5807  dmopab3  5876  rnopab3  5913  dfres2  6008  restidsing  6020  fununi  6575  dffv2  6937  dfsup2  9359  kmlem3  10075  recmulnq  10887  dmcuts  27799  nbgrel  29425  shne0i  31535  13an22anass  32549  ssiun3  32644  ind1a  32948  bnj1304  34994  bnj1253  35192  dfrecs2  36163  icorempo  37603  inxprnres  38546  disjressuc2  38659  dalem20  40066  ralopabb  43764  rp-isfinite6  43871  rababg  43927  nregmodel  45370  ssrabf  45470  ralfal  45517