Theorem 3imtr4i 201

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 121	. 2 |- ( ch -> ps )
4		3imtr4.3	. 2 |- ( th <-> ps )
5	3, 4	sylibr 134	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:  dcn  844  stdcn  849  xordc1  1413  hbxfrbi  1495  nfalt  1601  19.29r  1644  19.31r  1704  sbimi  1787  spsbbi  1867  sbi2v  1916  euan  2110  2exeu  2146  ralimi2  2566  reximi2  2602  r19.28av  2642  r19.29r  2644  elex  2783  rmoan  2973  rmoimi2  2976  sseq2  3217  rabss2  3276  unssdif  3408  inssdif  3409  unssin  3412  inssun  3413  rabn0r  3487  undif4  3523  ssdif0im  3525  inssdif0im  3528  ssundifim  3544  ralf0  3563  prmg  3754  difprsnss  3771  snsspw  3805  pwprss  3846  pwtpss  3847  uniin  3870  intss  3906  iuniin  3937  iuneq1  3940  iuneq2  3943  iundif2ss  3993  iinuniss  4010  iunpwss  4019  intexrabim  4198  exmidundif  4251  exmidundifim  4252  exss  4272  pwunss  4331  soeq2  4364  ordunisuc2r  4563  peano5  4647  reliin  4798  coeq1  4836  coeq2  4837  cnveq  4853  dmeq  4879  dmin  4887  dmcoss  4949  rncoeq  4953  resiexg  5005  dminss  5098  imainss  5099  dfco2a  5184  euiotaex  5249  eliotaeu  5261  fundif  5319  fununi  5343  fof  5500  f1ocnv  5537  rexrnmpt  5725  isocnv  5882  isotr  5887  oprabid  5978  dmtpos  6344  tposfn  6361  smores  6380  eqer  6654  ixpeq2  6801  enssdom  6855  fiprc  6909  fiintim  7030  ltexprlemlol  7717  ltexprlemupu  7719  recexgt0  8655  peano2uz2  9482  eluzp1p1  9676  peano2uz  9706  zq  9749  ubmelfzo  10331  frecuzrdgtcl  10559  frecuzrdgfunlem  10566  expclzaplem  10710  hashfiv01gt1  10929  wrdeq  11018  fsum2dlemstep  11778  fprod2dlemstep  11966  sin02gt0  12108  qredeu  12452  prmdc  12485  subrngrng  13997  lgslem3  15512  bj-stim  15719  bj-stan  15720  bj-stal  15722  bj-nfalt  15737  bj-indint  15904  tridceq  16032