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  1467  dcfromcon  1468  dcfrompeirce  1469  cbv1  1768  cbv1v  1770  moimv  2120  hblem  2313  tfi  4631  smores  6380  idssen  6870  suplocsrlem  7923  bezoutlemle  12362  limcmpted  15168  sincosq3sgn  15333  fsumdvdsmul  15496  subctctexmid  15974  dcapnconstALT  16038