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  850  stdcn  855  ifpdc  988  xordc1  1438  hbxfrbi  1521  nfalt  1627  19.29r  1670  19.31r  1729  sbimi  1813  spsbbi  1893  sbi2v  1943  euan  2139  2exeu  2175  ralimi2  2604  reximi2  2640  r19.28av  2681  r19.29r  2683  elex  2827  rmoan  3019  rmoimi2  3022  sseq2  3264  rabss2  3323  unssdif  3458  inssdif  3459  unssin  3462  inssun  3463  rabn0r  3537  undif4  3573  ssdif0im  3575  inssdif0im  3578  ssundifim  3595  ralf0  3614  prmg  3816  difprsnss  3834  snsspw  3870  pwprss  3912  pwtpss  3913  uniin  3936  intss  3972  iuniin  4003  iuneq1  4006  iuneq2  4009  iundif2ss  4059  iinuniss  4076  iunpwss  4085  intexrabim  4267  exmidundif  4321  exmidundifim  4322  exss  4345  pwunss  4406  soeq2  4439  ordunisuc2r  4638  peano5  4722  reliin  4876  coeq1  4914  coeq2  4915  cnveq  4931  dmeq  4958  dmin  4966  dmcoss  5029  rncoeq  5033  resiexg  5085  dminss  5179  imainss  5180  dfco2a  5265  euiotaex  5331  eliotaeu  5343  fundif  5402  fununi  5426  fof  5592  f1ocnv  5629  rexrnmpt  5822  isocnv  5986  isotr  5991  oprabid  6084  dmtpos  6489  tposfn  6506  smores  6525  eqer  6801  ixpeq2  6949  enssdom  7003  fiprc  7059  fiintim  7193  ltexprlemlol  7919  ltexprlemupu  7921  recexgt0  8856  peano2uz2  9688  eluzp1p1  9883  peano2uz  9918  zq  9961  ubmelfzo  10549  frecuzrdgtcl  10778  frecuzrdgfunlem  10785  expclzaplem  10929  hashfiv01gt1  11149  hashfibclem  11210  wrdeq  11250  fsum2dlemstep  12124  fprod2dlemstep  12312  sin02gt0  12454  qredeu  12798  prmdc  12831  subrngrng  14364  lgslem3  15892  clwwlkccat  16413  clwwlknonccat  16445  bj-stim  16535  bj-stan  16536  bj-stal  16538  bj-nfalt  16553  bj-indint  16718  tridceq  16858