Theorem 3bitr3ri 291

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

Hypotheses

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

Assertion

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

Proof of Theorem 3bitr3ri

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

Syntax hints:   <-> wb 196

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 197

This theorem is referenced by:  bigolden  976  2eu8  2560  2ralor  3109  sbcco  3458  symdifass  3853  dfiin2g  4553  zfpair  4904  dffun6f  5902  fsplit  7282  axdc3lem4  9275  istrkg2ld  25359  legso  25494  disjunsn  29407  gtiso  29478  fpwrelmapffslem  29507  qqhre  30064  dfpo2  31645  dfdm5  31676  dfrn5  31677  brimg  32044  dfrecs2  32057  poimirlem25  33434  cdlemefrs29bpre0  35684  cdlemftr3  35853  dffrege115  38272  brco3f1o  38331  elnev  38639  2reu8  41192