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  1512  ssrab  4096  copsex2gb  5830  relop  5875  dmopab3  5944  dfres2  6070  restidsing  6082  fununi  6653  dffv2  7017  dfsup2  9513  kmlem3  10222  recmulnq  11033  dmscut  27874  nbgrel  29375  shne0i  31480  13an22anass  32493  ssiun3  32581  cnvoprabOLD  32734  ind1a  33983  bnj1304  34795  bnj1253  34993  dfrecs2  35914  icorempo  37317  inxprnres  38248  disjressuc2  38344  dalem20  39650  ralopabb  43373  rp-isfinite6  43480  rababg  43536  ssrabf  45016  ralfal  45066