Theorem 3bitr2ri 301

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

Syntax hints:   ↔ wb 207

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 208

This theorem is referenced by:  xorass  1522  ssrab  4009  copsex2gb  5756  relop  5799  dmopab3  5868  rnopab3  5905  dfres2  6000  restidsing  6012  fununi  6567  dffv2  6929  dfsup2  9354  kmlem3  10073  recmulnq  10885  ind1a  12168  dmcuts  27808  nbgrel  29434  shne0i  31544  13an22anass  32558  ssiun3  32654  bnj1304  35008  bnj1253  35206  dfrecs2  36185  icorempo  37720  inxprnres  38672  disjressuc2  38785  dalem20  40192  ralopabb  43862  rp-isfinite6  43969  rababg  44025  nregmodel  45468  ssrabf  45568  ralfal  45615