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  4197  exmidundif  4250  exmidundifim  4251  exss  4271  pwunss  4330  soeq2  4363  ordunisuc2r  4562  peano5  4646  reliin  4797  coeq1  4835  coeq2  4836  cnveq  4852  dmeq  4878  dmin  4886  dmcoss  4948  rncoeq  4952  resiexg  5004  dminss  5097  imainss  5098  dfco2a  5183  euiotaex  5248  eliotaeu  5260  fundif  5318  fununi  5342  fof  5498  f1ocnv  5535  rexrnmpt  5723  isocnv  5880  isotr  5885  oprabid  5976  dmtpos  6342  tposfn  6359  smores  6378  eqer  6652  ixpeq2  6799  enssdom  6853  fiprc  6907  fiintim  7028  ltexprlemlol  7715  ltexprlemupu  7717  recexgt0  8653  peano2uz2  9480  eluzp1p1  9674  peano2uz  9704  zq  9747  ubmelfzo  10329  frecuzrdgtcl  10557  frecuzrdgfunlem  10564  expclzaplem  10708  hashfiv01gt1  10927  wrdeq  11016  fsum2dlemstep  11745  fprod2dlemstep  11933  sin02gt0  12075  qredeu  12419  prmdc  12452  subrngrng  13964  lgslem3  15479  bj-stim  15686  bj-stan  15687  bj-stal  15689  bj-nfalt  15704  bj-indint  15871  tridceq  15999