Theorem 3imtr4i 257

Description: A mixed syllogism inference, useful for applying a definition to both sides of an implication. (Contributed by NM, 5-Aug-1993.)

Hypotheses

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

Assertion

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

Proof of Theorem 3imtr4i

Step	Hyp	Ref	Expression
1		3imtr4.2	. . 3 |- (ch <-> ph)
2		3imtr4.1	. . 3 |- (ph -> ps)
3	1, 2	sylbi 187	. 2 |- (ch -> ps)
4		3imtr4.3	. 2 |- (th <-> ps)
5	3, 4	sylibr 203	1 |- (ch -> th)

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 177

This theorem is referenced by:  hbxfrbi  1568  19.30  1604  sbimi  1652  hba1  1786  nfimdOLD  1809  euan  2261  ralimi2  2686  reximi2  2720  r19.28av  2753  r19.29r  2755  r19.30  2756  elex  2867  rmoan  3034  rmoimi2  3037  sseq2  3293  rabss2  3349  undif4  3607  r19.2zb  3640  ralf0  3656  difprsnss  3846  snsspw  3877  uniin  3911  intss  3947  iuniin  3979  iuneq1  3982  iuneq2  3985  iunpwss  4055  iotaex  4356  peano2  4403  nnpw1ex  4484  spfininduct  4540  brex  4689  coeq1  4874  coeq2  4875  cnveq  4886  dmeq  4907  dmin  4913  brelrn  4960  dmcoss  4971  rncoeq  4975  dminss  5041  imainss  5042  dfco2a  5081  funmo  5125  funeq  5127  funun  5146  fununi  5160  2elresin  5194  fco  5231  f1co  5264  fof  5269  foco  5279  f1ores  5300  f1oco  5308  fvpr2  5450  isocnv  5491  isotr  5495  oprabid  5550  fntxp  5804  fnpprod  5843  f1opprod  5844  ider  5943  ssetpov  5944  eqer  5961  map0  6025  unen  6048  pw1fin  6169  cenc  6181  lecidg  6196  lec0cg  6198  lecncvg  6199  sbth  6206  addlec  6208  nc0le1  6216  ce2le  6233  dmfrec  6316  scancan  6331