Theorem 3imtr3i 200

Description: A mixed syllogism inference, useful for removing a definition from both sides of an implication. (Contributed by NM, 10-Aug-1994.)

Hypotheses

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

Assertion

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

Proof of Theorem 3imtr3i

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

Syntax hints:   -> wi 4   <-> wb 105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  dcfromnotnotr  1493  dcfromcon  1494  dcfrompeirce  1495  cbv1  1794  cbv1v  1796  moimv  2149  hblem  2342  tfi  4709  fresaunres1disj  5551  smores  6536  idssen  7029  suplocsrlem  8139  bezoutlemle  12729  limcmpted  15654  sincosq3sgn  15819  fsumdvdsmul  15985  subctctexmid  16900  dcapnconstALT  16974