Theorem 3bitr3ri 305

Description: A chained inference from transitive law for logical equivalence. (Contributed by NM, 21-Jun-1993.)

Hypotheses

Ref	Expression
3bitr3i.1	⊢ (𝜑 ↔ 𝜓)
3bitr3i.2	⊢ (𝜑 ↔ 𝜒)
3bitr3i.3	⊢ (𝜓 ↔ 𝜃)

Assertion

Ref	Expression
3bitr3ri	⊢ (𝜃 ↔ 𝜒)

Proof of Theorem 3bitr3ri

Step	Hyp	Ref	Expression
1		3bitr3i.3	. 2 ⊢ (𝜓 ↔ 𝜃)
2		3bitr3i.1	. . 3 ⊢ (𝜑 ↔ 𝜓)
3		3bitr3i.2	. . 3 ⊢ (𝜑 ↔ 𝜒)
4	2, 3	bitr3i 280	. 2 ⊢ (𝜓 ↔ 𝜒)
5	1, 4	bitr3i 280	1 ⊢ (𝜃 ↔ 𝜒)

This proof depends on syntax axioms:   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  bigolden  1044  sb8f  2386  2eu8  2686  sbccow  3765  sbcco  3768  dfiin2g  4992  zfpair  5387  dfpo2  6317  dffun6f  6573  fnssintima  7395  fsplit  8155  axdc3lem4  10558  addsuniflem  28417  addsasslem1  28419  addsasslem2  28420  addsdilem1  28567  addsdilem2  28568  mulsasslem1  28579  mulsasslem2  28580  elreno2  28911  renegscl  28914  istrkg2ld  28952  legso  29092  disjunsn  33260  gtiso  33365  fpwrelmapffslem  33394  qqhre  34722  satfdm  36301  dfdm5  36715  dfrn5  36716  brimg  36877  dfrecs2  36892  bj-elinxp  38138  poimirlem25  38755  cdlemefrs29bpre0  41645  cdlemftr3  41814  dffrege115  45170  brco3f1o  45225  2reu8  48388  ichbi12i  48747  iuneq0  50135  i0oii  50239  setc1onsubc  50945