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 552  sbal 1347  onminex 3020  tfinds2 3165  funeu2 3538  idssen 4406  xpen 4488  rankss 4688  rankxplim3 4714  distrlem3pr 5129  ltadd2 5590  ltmul1i 5821  infmsup 6068  nnwos 6460  csbfsum 7027  climunii 7098  efseq0ex 7311  efltb 7407  sincosq3sgn 8706  cosh111lem2 8715  hlimunii 9108  adjbdlnt 10016

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