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  1516  ssrab  4023  copsex2gb  5746  relop  5790  dmopab3  5859  rnopab3  5896  dfres2  5990  restidsing  6002  fununi  6556  dffv2  6917  dfsup2  9328  kmlem3  10044  recmulnq  10855  dmscut  27753  nbgrel  29319  shne0i  31426  13an22anass  32441  ssiun3  32536  ind1a  32838  bnj1304  34829  bnj1253  35027  dfrecs2  35990  icorempo  37391  inxprnres  38332  disjressuc2  38426  dalem20  39738  ralopabb  43450  rp-isfinite6  43557  rababg  43613  nregmodel  45056  ssrabf  45157  ralfal  45204