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  4012  copsex2gb  5755  relop  5799  dmopab3  5868  rnopab3  5905  dfres2  6000  restidsing  6012  fununi  6567  dffv2  6929  dfsup2  9350  kmlem3  10066  recmulnq  10878  ind1a  12161  dmcuts  27797  nbgrel  29423  shne0i  31534  13an22anass  32548  ssiun3  32643  bnj1304  34977  bnj1253  35175  dfrecs2  36148  icorempo  37681  inxprnres  38633  disjressuc2  38746  dalem20  40153  ralopabb  43856  rp-isfinite6  43963  rababg  44019  nregmodel  45462  ssrabf  45562  ralfal  45609