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  1513  ssrab  4017  copsex2gb  5735  relop  5779  dmopab3  5848  dfres2  5968  restidsing  5979  fununi  6545  dffv2  6902  dfsup2  9273  kmlem3  9981  recmulnq  10793  nbgrel  27816  shne0i  29919  ssiun3  31006  cnvoprabOLD  31163  ind1a  32093  bnj1304  32904  bnj1253  33102  dmscut  34063  dfrecs2  34310  icorempo  35578  inxprnres  36509  disjressuc2  36606  dalem20  37912  rp-isfinite6  41346  rababg  41402  ssrabf  42885