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  4022  copsex2gb  5791  relop  5834  dmopab3  5907  rnopab3  5944  dfres2  6041  restidsing  6053  fununi  6612  dffv2  6977  dfsup2  9418  kmlem3  10159  recmulnq  10977  ind1a  12257  dmcuts  28064  nbgrel  29808  shne0i  31937  ssiun3  33040  bnj1304  35336  bnj1253  35534  dfrecs2  36537  icorempo  38113  inxprnres  39054  disjressuc2  39167  dalem20  40574  ralopabb  44259  rp-isfinite6  44366  rababg  44422  nregmodel  45848  ssrabf  45954  ralfal  46001