Theorem 3bitr3i 266

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

Hypotheses

Ref	Expression
3bitr3i.1	|- (ph <-> ps)
3bitr3i.2	|- (ph <-> ch)
3bitr3i.3	|- (ps <-> th)

Assertion

Ref	Expression
3bitr3i	|- (ch <-> th)

Proof of Theorem 3bitr3i

Step	Hyp	Ref	Expression
1		3bitr3i.2	. . 3 |- (ph <-> ch)
2		3bitr3i.1	. . 3 |- (ph <-> ps)
3	1, 2	bitr3i 242	. 2 |- (ch <-> ps)
4		3bitr3i.3	. 2 |- (ps <-> th)
5	3, 4	bitri 240	1 |- (ch <-> th)

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  elsb1  2103  elsb2  2104  sbcom2  2114  dfsb7  2119  sb7f  2120  eq2tri  2412  eqsb1  2454  clelsb1  2455  clelsb2  2456  r19.35  2759  ralcom4  2878  rexcom4  2879  ceqsralt  2883  gencbvex  2902  gencbval  2904  ceqsrexbv  2974  euind  3024  reuind  3040  sbccomlem  3117  sbccom  3118  ab0  3570  difcom  3635  uniintsn  3964  pw1in  4165  dfimak2  4299  addcass  4416  elswap  4741  elxp2  4803  eqbrriv  4852  opelcnv  4894  dm0rn0  4922  opelres  4951  rninxp  5061  fununi  5161  dfoprab2  5559  opsnelsi  5775  oteltxp  5783  funsex  5829  pw1fnex  5853  brpw1fn  5855  nenpw1pwlem1  6085  lecex  6116  el2c  6192  brtcfn  6247