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  5560  f1ocnv  5597  rexrnmpt  5791  isocnv  5955  isotr  5960  oprabid  6053  dmtpos  6425  tposfn  6442  smores  6461  eqer  6737  ixpeq2  6884  enssdom  6938  fiprc  6993  fiintim  7126  ltexprlemlol  7825  ltexprlemupu  7827  recexgt0  8763  peano2uz2  9590  eluzp1p1  9785  peano2uz  9820  zq  9863  ubmelfzo  10449  frecuzrdgtcl  10678  frecuzrdgfunlem  10685  expclzaplem  10829  hashfiv01gt1  11048  wrdeq  11142  fsum2dlemstep  12016  fprod2dlemstep  12204  sin02gt0  12346  qredeu  12690  prmdc  12723  subrngrng  14238  lgslem3  15758  clwwlkccat  16279  clwwlknonccat  16311  bj-stim  16401  bj-stan  16402  bj-stal  16404  bj-nfalt  16419  bj-indint  16585  tridceq  16720