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  1509  ssrab  4066  copsex2gb  5804  relop  5849  dmopab3  5918  dfres2  6042  restidsing  6054  fununi  6626  dffv2  6989  dfsup2  9480  kmlem3  10188  recmulnq  10998  dmscut  27838  nbgrel  29273  shne0i  31378  13an22anass  32391  ssiun3  32479  cnvoprabOLD  32634  ind1a  33865  bnj1304  34677  bnj1253  34875  dfrecs2  35787  icorempo  37071  inxprnres  38003  disjressuc2  38099  dalem20  39405  ralopabb  43115  rp-isfinite6  43222  rababg  43278  ssrabf  44752  ralfal  44802