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  4073  copsex2gb  5816  relop  5861  dmopab3  5930  rnopab3  5967  dfres2  6059  restidsing  6071  fununi  6641  dffv2  7004  dfsup2  9484  kmlem3  10193  recmulnq  11004  dmscut  27856  nbgrel  29357  shne0i  31467  13an22anass  32483  ssiun3  32571  ind1a  32844  bnj1304  34833  bnj1253  35031  dfrecs2  35951  icorempo  37352  inxprnres  38293  disjressuc2  38389  dalem20  39695  ralopabb  43424  rp-isfinite6  43531  rababg  43587  ssrabf  45119  ralfal  45166