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  4019  copsex2gb  5784  relop  5828  dmopab3  5901  rnopab3  5938  dfres2  6035  restidsing  6047  fununi  6607  dffv2  6972  dfsup2  9420  kmlem3  10212  recmulnq  11030  ind1a  12312  dmcuts  28159  nbgrel  29903  shne0i  32032  ssiun3  33135  bnj1304  35432  bnj1253  35630  dfrecs2  36684  icorempo  38242  inxprnres  39198  disjressuc2  39311  dalem20  40718  ralopabb  44370  rp-isfinite6  44477  rababg  44533  nregmodel  45959  ssrabf  46072  ralfal  46119