Theorem 3bitr2ri 302

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 280	. 2 ⊢ (𝜑 ↔ 𝜒)
4		3bitr2i.3	. 2 ⊢ (𝜒 ↔ 𝜃)
5	3, 4	bitr2i 278	1 ⊢ (𝜃 ↔ 𝜑)

Syntax hints:   ↔ wb 208

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 209

This theorem is referenced by:  xorass  1504  nororOLD  1525  ssrab  4048  copsex2gb  5673  relop  5715  dmopab3  5782  dfres2  5903  restidsing  5916  fununi  6423  dffv2  6750  dfsup2  8902  kmlem3  9572  recmulnq  10380  nbgrel  27116  shne0i  29219  ssiun3  30304  cnvoprabOLD  30450  ind1a  31273  bnj1304  32086  bnj1253  32284  dmscut  33267  dfrecs2  33406  icorempo  34626  inxprnres  35543  dalem20  36823  rp-isfinite6  39877  rababg  39926  ssrabf  41374