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  4026  copsex2gb  5753  relop  5797  dmopab3  5866  rnopab3  5902  dfres2  5996  restidsing  6008  fununi  6561  dffv2  6922  dfsup2  9353  kmlem3  10066  recmulnq  10877  dmscut  27740  nbgrel  29303  shne0i  31410  13an22anass  32426  ssiun3  32520  ind1a  32815  bnj1304  34788  bnj1253  34986  dfrecs2  35926  icorempo  37327  inxprnres  38268  disjressuc2  38362  dalem20  39675  ralopabb  43387  rp-isfinite6  43494  rababg  43550  nregmodel  44994  ssrabf  45095  ralfal  45142