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  1517  ssrab  4011  copsex2gb  5762  relop  5805  dmopab3  5874  rnopab3  5911  dfres2  6006  restidsing  6018  fununi  6573  dffv2  6935  dfsup2  9357  kmlem3  10075  recmulnq  10887  ind1a  12170  dmcuts  27783  nbgrel  29409  shne0i  31519  13an22anass  32533  ssiun3  32628  bnj1304  34961  bnj1253  35159  dfrecs2  36132  icorempo  37667  inxprnres  38619  disjressuc2  38732  dalem20  40139  ralopabb  43838  rp-isfinite6  43945  rababg  44001  nregmodel  45444  ssrabf  45544  ralfal  45591