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  1514  ssrab  4070  copsex2gb  5806  relop  5850  dmopab3  5919  dfres2  6041  restidsing  6052  fununi  6623  dffv2  6986  dfsup2  9441  kmlem3  10149  recmulnq  10961  dmscut  27320  nbgrel  28635  shne0i  30739  13an22anass  31744  ssiun3  31828  cnvoprabOLD  31983  ind1a  33086  bnj1304  33899  bnj1253  34097  dfrecs2  34991  icorempo  36318  inxprnres  37247  disjressuc2  37344  dalem20  38650  ralopabb  42244  rp-isfinite6  42351  rababg  42407  ssrabf  43885  ralfal  43937