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  1544  ssrab  3996  copsex2gb  5783  relop  5827  dmopab3  5900  rnopab3  5937  dfres2  6032  restidsing  6044  fununi  6615  dffv2  6980  dfsup2  9439  kmlem3  10234  recmulnq  11052  ind1a  12334  dmcuts  28182  nbgrel  29926  shne0i  32055  ssiun3  33200  bnj1304  35495  bnj1253  35693  dfrecs2  36806  icorempo  38367  inxprnres  39323  disjressuc2  39436  dalem20  40843  ralopabb  44505  rp-isfinite6  44612  rababg  44668  nregmodel  46100  ssrabf  46222  ralfal  46269