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  4048  copsex2gb  5785  relop  5830  dmopab3  5899  rnopab3  5936  dfres2  6028  restidsing  6040  fununi  6611  dffv2  6974  dfsup2  9456  kmlem3  10167  recmulnq  10978  dmscut  27775  nbgrel  29319  shne0i  31429  13an22anass  32445  ssiun3  32539  ind1a  32836  bnj1304  34850  bnj1253  35048  dfrecs2  35968  icorempo  37369  inxprnres  38310  disjressuc2  38406  dalem20  39712  ralopabb  43435  rp-isfinite6  43542  rababg  43598  ssrabf  45138  ralfal  45185