Theorem 3bitr3i 266

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

Hypotheses

Ref	Expression
3bitr3i.1	⊢ (φ ↔ ψ)
3bitr3i.2	⊢ (φ ↔ χ)
3bitr3i.3	⊢ (ψ ↔ θ)

Assertion

Ref	Expression
3bitr3i	⊢ (χ ↔ θ)

Proof of Theorem 3bitr3i

Step	Hyp	Ref	Expression
1		3bitr3i.2	. . 3 ⊢ (φ ↔ χ)
2		3bitr3i.1	. . 3 ⊢ (φ ↔ ψ)
3	1, 2	bitr3i 242	. 2 ⊢ (χ ↔ ψ)
4		3bitr3i.3	. 2 ⊢ (ψ ↔ θ)
5	3, 4	bitri 240	1 ⊢ (χ ↔ θ)

Syntax hints:   ↔ wb 176

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 177

This theorem is referenced by:  an12  772  cadan  1392  19.35  1600  cbval2  2004  cbvex2  2005  sbco2d  2087  equsb3  2102  elsb3  2103  elsb4  2104  sbcom2  2114  dfsb7  2119  sb7f  2120  eq2tri  2412  eqsb3  2454  clelsb3  2455  r19.35  2758  ralcom4  2877  rexcom4  2878  ceqsralt  2882  gencbvex  2901  gencbval  2903  ceqsrexbv  2973  euind  3023  reuind  3039  sbccomlem  3116  sbccom  3117  ab0  3569  difcom  3634  uniintsn  3963  pw1in  4164  dfimak2  4298  addcass  4415  elswap  4740  elxp2  4802  eqbrriv  4851  opelcnv  4893  dm0rn0  4921  opelres  4950  rninxp  5060  fununi  5160  dfoprab2  5558  opsnelsi  5774  oteltxp  5782  funsex  5828  pw1fnex  5852  brpw1fn  5854  nenpw1pwlem1  6084  lecex  6115  el2c  6191  brtcfn  6246