Theorem 3imtr4i 190

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 114	. 2 |- (ch -> ps)
4		3imtr4.3	. 2 |- (th <-> ps)
5	3, 4	sylibr 137	1 |- (ch -> th)

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

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  dcn  745  dcan  841  xordc1  1281  hbxfrbi  1358  nfalt  1467  19.29r  1509  19.31r  1568  sbimi  1644  spsbbi  1722  sbi2v  1769  euan  1953  2exeu  1989  ralimi2  2375  reximi2  2409  r19.28av  2443  r19.29r  2445  elex  2560  rmoan  2733  rmoimi2  2736  sseq2  2961  rabss2  3017  unssdif  3166  inssdif  3167  unssin  3170  inssun  3171  rabn0r  3238  undif4  3278  ssdif0im  3280  inssdif0im  3285  ssundifim  3300  ralf0  3318  prmg  3480  difprsnss  3493  snsspw  3526  pwprss  3567  pwtpss  3568  uniin  3591  intss  3627  iuniin  3658  iuneq1  3661  iuneq2  3664  iundif2ss  3713  iinuniss  3728  iunpwss  3734  intexrabim  3898  exss  3954  pwunss  4011  soeq2  4044  ordunisuc2r  4205  peano5  4264  reliin  4402  coeq1  4436  coeq2  4437  cnveq  4452  dmeq  4478  dmin  4486  dmcoss  4544  rncoeq  4548  resiexg  4596  dminss  4681  imainss  4682  dfco2a  4764  euiotaex  4826  fununi  4910  fof  5049  f1ocnv  5082  rexrnmpt  5253  isocnv  5394  isotr  5399  oprabid  5480  dmtpos  5812  tposfn  5829  smores  5848  eqer  6074  enssdom  6178  fiprc  6228  ltexprlemlol  6576  ltexprlemupu  6578  recexgt0  7364  peano2uz2  8121  eluzp1p1  8274  peano2uz  8302  zq  8337  elfzmlbmOLD  8759  ubmelfzo  8826  frecuzrdgfn  8879  expclzaplem  8933  bj-indint  9390  peano5setOLD  9400