Theorem 3bitr2ri 300

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  1511  ssrab  4006  copsex2gb  5716  relop  5759  dmopab3  5828  dfres2  5949  restidsing  5962  fununi  6509  dffv2  6863  dfsup2  9203  kmlem3  9908  recmulnq  10720  nbgrel  27707  shne0i  29810  ssiun3  30898  cnvoprabOLD  31055  ind1a  31987  bnj1304  32799  bnj1253  32997  dmscut  34005  dfrecs2  34252  icorempo  35522  inxprnres  36427  dalem20  37707  rp-isfinite6  41125  rababg  41181  ssrabf  42664