Theorem 3imtr3 218

Description: A mixed syllogism inference, useful for removing a definition from both sides of an implication.

Hypotheses

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

Assertion

Ref	Expression
3imtr3	|- (ch -> th)

Proof of Theorem 3imtr3

Step	Hyp	Ref	Expression
1		3imtr3.2	. . 3 |- (ph <-> ch)
2		3imtr3.1	. . 3 |- (ph -> ps)
3	1, 2	sylbir 201	. 2 |- (ch -> ps)
4		3imtr3.3	. 2 |- (ps <-> th)
5	3, 4	sylib 198	1 |- (ch -> th)

Syntax hints:   -> wi 3   <-> wb 146

This theorem is referenced by:  3imtr3g 551  sbal 1345  onminex 3015  tfinds2 3160  funeu2 3530  idssen 4393  xpen 4474  rankss 4668  rankxplim3 4694  distrlem3pr 5109  ltadd2 5572  ltmul1i 5785  infmsup 6023  nnwos 6400  csbfsum 6973  climunii 7043  efseq0ex 7261  efltb 7356  sincosq3sgn 8642  cosh111lem2 8649  hlimunii 9047  adjbdlnt 9954

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 147

Copyright terms: Public domain