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  2385  2eu8  2685  sbccow  3765  sbcco  3768  dfiin2g  4993  zfpair  5390  dfpo2  6298  dffun6f  6552  fnssintima  7369  fsplit  8118  axdc3lem4  10459  addsuniflem  28274  addsasslem1  28276  addsasslem2  28277  addsdilem1  28424  addsdilem2  28425  mulsasslem1  28436  mulsasslem2  28437  elreno2  28768  renegscl  28771  istrkg2ld  28809  legso  28949  disjunsn  33075  gtiso  33181  fpwrelmapffslem  33211  qqhre  34538  satfdm  35956  dfdm5  36360  dfrn5  36361  brimg  36522  dfrecs2  36537  poimirlem25  38402  cdlemefrs29bpre0  41277  cdlemftr3  41446  dffrege115  44826  brco3f1o  44881  2reu8  48008  ichbi12i  48368  iuneq0  49755  i0oii  49854  setc1onsubc  50536