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  1534  ssrab  4022  copsex2gb  5775  relop  5818  dmopab3  5891  rnopab3  5928  dfres2  6025  restidsing  6037  fununi  6590  dffv2  6956  dfsup2  9383  kmlem3  10102  recmulnq  10915  ind1a  12199  dmcuts  27871  nbgrel  29497  shne0i  31607  13an22anass  32621  ssiun3  32717  bnj1304  35074  bnj1253  35272  dfrecs2  36260  icorempo  37805  inxprnres  38757  disjressuc2  38870  dalem20  40277  ralopabb  43947  rp-isfinite6  44054  rababg  44110  nregmodel  45553  ssrabf  45652  ralfal  45699