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 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  1515  ssrab  4071  copsex2gb  5807  relop  5851  dmopab3  5920  dfres2  6042  restidsing  6053  fununi  6624  dffv2  6987  dfsup2  9439  kmlem3  10147  recmulnq  10959  dmscut  27312  nbgrel  28597  shne0i  30701  13an22anass  31706  ssiun3  31790  cnvoprabOLD  31945  ind1a  33017  bnj1304  33830  bnj1253  34028  dfrecs2  34922  icorempo  36232  inxprnres  37161  disjressuc2  37258  dalem20  38564  ralopabb  42162  rp-isfinite6  42269  rababg  42325  ssrabf  43803  ralfal  43855