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:  13an22anassOLD  1380  xorass  1545  ssrab  3999  copsex2gb  5790  relop  5835  dmopab3  5909  rnopab3  5946  dfres2  6046  restidsing  6058  fununi  6640  dffv2  7006  dfsup2  9466  kmlem3  10261  recmulnq  11079  ind1a  12361  dmcuts  28210  nbgrel  29954  shne0i  32083  ssiun3  33228  bnj1304  35532  bnj1253  35730  dfrecs2  36905  icorempo  38479  inxprnres  39433  disjressuc2  39546  dalem20  40953  ralopabb  44615  rp-isfinite6  44722  rababg  44778  nregmodel  46213  ssrabf  46344  ralfal  46391