Theorem 3bitr2ri 303

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

Syntax hints:   ↔ wb 209

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 210

This theorem is referenced by:  13an22anass  1379  xorass  1545  ssrab  4026  copsex2gb  5795  relop  5838  dmopab3  5911  rnopab3  5948  dfres2  6045  restidsing  6057  fununi  6613  dffv2  6978  dfsup2  9405  kmlem3  10137  recmulnq  10950  ind1a  12230  dmcuts  27965  nbgrel  29671  shne0i  31781  ssiun3  32884  bnj1304  35188  bnj1253  35386  dfrecs2  36423  icorempo  37978  inxprnres  38928  disjressuc2  39041  dalem20  40448  ralopabb  44120  rp-isfinite6  44227  rababg  44283  nregmodel  45709  ssrabf  45815  ralfal  45862