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  847  stdcn  852  ifpdc  985  xordc1  1435  hbxfrbi  1518  nfalt  1624  19.29r  1667  19.31r  1727  sbimi  1810  spsbbi  1890  sbi2v  1939  euan  2134  2exeu  2170  ralimi2  2590  reximi2  2626  r19.28av  2667  r19.29r  2669  elex  2811  rmoan  3003  rmoimi2  3006  sseq2  3248  rabss2  3307  unssdif  3439  inssdif  3440  unssin  3443  inssun  3444  rabn0r  3518  undif4  3554  ssdif0im  3556  inssdif0im  3559  ssundifim  3575  ralf0  3594  prmg  3789  difprsnss  3806  snsspw  3842  pwprss  3884  pwtpss  3885  uniin  3908  intss  3944  iuniin  3975  iuneq1  3978  iuneq2  3981  iundif2ss  4031  iinuniss  4048  iunpwss  4057  intexrabim  4237  exmidundif  4290  exmidundifim  4291  exss  4313  pwunss  4374  soeq2  4407  ordunisuc2r  4606  peano5  4690  reliin  4841  coeq1  4879  coeq2  4880  cnveq  4896  dmeq  4923  dmin  4931  dmcoss  4994  rncoeq  4998  resiexg  5050  dminss  5143  imainss  5144  dfco2a  5229  euiotaex  5295  eliotaeu  5307  fundif  5365  fununi  5389  fof  5548  f1ocnv  5585  rexrnmpt  5778  isocnv  5935  isotr  5940  oprabid  6033  dmtpos  6402  tposfn  6419  smores  6438  eqer  6712  ixpeq2  6859  enssdom  6913  fiprc  6968  fiintim  7093  ltexprlemlol  7789  ltexprlemupu  7791  recexgt0  8727  peano2uz2  9554  eluzp1p1  9748  peano2uz  9778  zq  9821  ubmelfzo  10406  frecuzrdgtcl  10634  frecuzrdgfunlem  10641  expclzaplem  10785  hashfiv01gt1  11004  wrdeq  11093  fsum2dlemstep  11945  fprod2dlemstep  12133  sin02gt0  12275  qredeu  12619  prmdc  12652  subrngrng  14166  lgslem3  15681  bj-stim  16110  bj-stan  16111  bj-stal  16113  bj-nfalt  16128  bj-indint  16294  tridceq  16424