Theorem 3bitr2ri 303

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 281	. 2 ⊢ (𝜑 ↔ 𝜒)
4		3bitr2i.3	. 2 ⊢ (𝜒 ↔ 𝜃)
5	3, 4	bitr2i 279	1 ⊢ (𝜃 ↔ 𝜑)

This proof depends on syntax axioms:   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  13an22anass  1379  xorass  1545  ssrab  4028  copsex2gb  5798  relop  5841  dmopab3  5914  rnopab3  5951  dfres2  6048  restidsing  6060  fununi  6618  dffv2  6983  dfsup2  9414  kmlem3  10155  recmulnq  10967  ind1a  12247  dmcuts  28021  nbgrel  29727  shne0i  31837  ssiun3  32940  bnj1304  35239  bnj1253  35437  dfrecs2  36463  icorempo  38038  inxprnres  38988  disjressuc2  39101  dalem20  40508  ralopabb  44178  rp-isfinite6  44285  rababg  44341  nregmodel  45767  ssrabf  45873  ralfal  45920