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  1490  dcfromcon  1491  dcfrompeirce  1492  cbv1  1791  cbv1v  1793  moimv  2144  hblem  2337  tfi  4674  smores  6438  idssen  6928  suplocsrlem  7995  bezoutlemle  12529  limcmpted  15337  sincosq3sgn  15502  fsumdvdsmul  15665  subctctexmid  16366  dcapnconstALT  16430