Theorem 3bitr2ri 292

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

Syntax hints:   ↔ wb 198

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 199

This theorem is referenced by:  xorass  1492  ssrab  3939  copsex2gb  5529  relop  5571  dmopab3  5635  dfres2  5754  restidsing  5764  fununi  6262  dffv2  6584  dfsup2  8703  kmlem3  9372  recmulnq  10184  nbgrel  26825  shne0i  29006  ssiun3  30079  cnvoprabOLD  30215  ind1a  30928  bnj1304  31745  bnj1253  31940  dmscut  32799  dfrecs2  32938  icorempo  34080  inxprnres  34999  dalem20  36280  rp-isfinite6  39286  rababg  39301  ssrabf  40810