Theorem 3bitr2ri 299

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

Syntax hints:   ↔ wb 205

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 206

This theorem is referenced by:  xorass  1508  nororOLD  1531  ssrab  4002  copsex2gb  5705  relop  5748  dmopab3  5817  dfres2  5938  restidsing  5951  fununi  6493  dffv2  6845  dfsup2  9133  kmlem3  9839  recmulnq  10651  nbgrel  27610  shne0i  29711  ssiun3  30799  cnvoprabOLD  30957  ind1a  31887  bnj1304  32699  bnj1253  32897  dmscut  33932  dfrecs2  34179  icorempo  35449  inxprnres  36354  dalem20  37634  rp-isfinite6  41023  rababg  41070  ssrabf  42553