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  4023  copsex2gb  5755  relop  5799  dmopab3  5868  rnopab3  5905  dfres2  6000  restidsing  6012  fununi  6567  dffv2  6929  dfsup2  9347  kmlem3  10063  recmulnq  10875  dmcuts  27787  nbgrel  29413  shne0i  31523  13an22anass  32538  ssiun3  32633  ind1a  32938  bnj1304  34975  bnj1253  35173  dfrecs2  36144  icorempo  37556  inxprnres  38491  disjressuc2  38596  dalem20  39953  ralopabb  43652  rp-isfinite6  43759  rababg  43815  nregmodel  45258  ssrabf  45358  ralfal  45405