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  1515  ssrab  4039  copsex2gb  5772  relop  5817  dmopab3  5886  rnopab3  5923  dfres2  6015  restidsing  6027  fununi  6594  dffv2  6959  dfsup2  9402  kmlem3  10113  recmulnq  10924  dmscut  27730  nbgrel  29274  shne0i  31384  13an22anass  32400  ssiun3  32494  ind1a  32789  bnj1304  34816  bnj1253  35014  dfrecs2  35945  icorempo  37346  inxprnres  38287  disjressuc2  38381  dalem20  39694  ralopabb  43407  rp-isfinite6  43514  rababg  43570  nregmodel  45014  ssrabf  45115  ralfal  45162