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  1492  dcfromcon  1493  dcfrompeirce  1494  cbv1  1793  cbv1v  1795  moimv  2146  hblem  2339  tfi  4680  smores  6457  idssen  6949  suplocsrlem  8027  bezoutlemle  12578  limcmpted  15386  sincosq3sgn  15551  fsumdvdsmul  15714  subctctexmid  16601  dcapnconstALT  16666