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

Syntax hints:   ↔ wb 206

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 207

This theorem is referenced by:  xorass  1516  ssrab  4019  copsex2gb  5750  relop  5795  dmopab3  5864  rnopab3  5901  dfres2  5995  restidsing  6007  fununi  6562  dffv2  6923  dfsup2  9334  kmlem3  10050  recmulnq  10861  dmscut  27758  nbgrel  29325  shne0i  31435  13an22anass  32450  ssiun3  32545  ind1a  32847  bnj1304  34838  bnj1253  35036  dfrecs2  36001  icorempo  37402  inxprnres  38336  disjressuc2  38441  dalem20  39798  ralopabb  43509  rp-isfinite6  43616  rababg  43672  nregmodel  45115  ssrabf  45216  ralfal  45263