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  849  stdcn  854  ifpdc  987  xordc1  1437  hbxfrbi  1520  nfalt  1626  19.29r  1669  19.31r  1729  sbimi  1812  spsbbi  1892  sbi2v  1941  euan  2136  2exeu  2172  ralimi2  2592  reximi2  2628  r19.28av  2669  r19.29r  2671  elex  2814  rmoan  3006  rmoimi2  3009  sseq2  3251  rabss2  3310  unssdif  3442  inssdif  3443  unssin  3446  inssun  3447  rabn0r  3521  undif4  3557  ssdif0im  3559  inssdif0im  3562  ssundifim  3578  ralf0  3597  prmg  3794  difprsnss  3811  snsspw  3847  pwprss  3889  pwtpss  3890  uniin  3913  intss  3949  iuniin  3980  iuneq1  3983  iuneq2  3986  iundif2ss  4036  iinuniss  4053  iunpwss  4062  intexrabim  4243  exmidundif  4296  exmidundifim  4297  exss  4319  pwunss  4380  soeq2  4413  ordunisuc2r  4612  peano5  4696  reliin  4849  coeq1  4887  coeq2  4888  cnveq  4904  dmeq  4931  dmin  4939  dmcoss  5002  rncoeq  5006  resiexg  5058  dminss  5151  imainss  5152  dfco2a  5237  euiotaex  5303  eliotaeu  5315  fundif  5374  fununi  5398  fof  5559  f1ocnv  5596  rexrnmpt  5790  isocnv  5952  isotr  5957  oprabid  6050  dmtpos  6422  tposfn  6439  smores  6458  eqer  6734  ixpeq2  6881  enssdom  6935  fiprc  6990  fiintim  7123  ltexprlemlol  7822  ltexprlemupu  7824  recexgt0  8760  peano2uz2  9587  eluzp1p1  9782  peano2uz  9817  zq  9860  ubmelfzo  10445  frecuzrdgtcl  10674  frecuzrdgfunlem  10681  expclzaplem  10825  hashfiv01gt1  11044  wrdeq  11135  fsum2dlemstep  11996  fprod2dlemstep  12184  sin02gt0  12326  qredeu  12670  prmdc  12703  subrngrng  14218  lgslem3  15733  clwwlkccat  16254  clwwlknonccat  16286  bj-stim  16345  bj-stan  16346  bj-stal  16348  bj-nfalt  16363  bj-indint  16529  tridceq  16663