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  843  stdcn  848  xordc1  1404  hbxfrbi  1483  nfalt  1589  19.29r  1632  19.31r  1692  sbimi  1775  spsbbi  1855  sbi2v  1904  euan  2098  2exeu  2134  ralimi2  2554  reximi2  2590  r19.28av  2630  r19.29r  2632  elex  2771  rmoan  2960  rmoimi2  2963  sseq2  3203  rabss2  3262  unssdif  3394  inssdif  3395  unssin  3398  inssun  3399  rabn0r  3473  undif4  3509  ssdif0im  3511  inssdif0im  3514  ssundifim  3530  ralf0  3549  prmg  3739  difprsnss  3756  snsspw  3790  pwprss  3831  pwtpss  3832  uniin  3855  intss  3891  iuniin  3922  iuneq1  3925  iuneq2  3928  iundif2ss  3978  iinuniss  3995  iunpwss  4004  intexrabim  4182  exmidundif  4235  exmidundifim  4236  exss  4256  pwunss  4314  soeq2  4347  ordunisuc2r  4546  peano5  4630  reliin  4781  coeq1  4819  coeq2  4820  cnveq  4836  dmeq  4862  dmin  4870  dmcoss  4931  rncoeq  4935  resiexg  4987  dminss  5080  imainss  5081  dfco2a  5166  euiotaex  5231  eliotaeu  5243  fununi  5322  fof  5476  f1ocnv  5513  rexrnmpt  5701  isocnv  5854  isotr  5859  oprabid  5950  dmtpos  6309  tposfn  6326  smores  6345  eqer  6619  ixpeq2  6766  enssdom  6816  fiprc  6869  fiintim  6985  ltexprlemlol  7662  ltexprlemupu  7664  recexgt0  8599  peano2uz2  9424  eluzp1p1  9618  peano2uz  9648  zq  9691  ubmelfzo  10267  frecuzrdgtcl  10483  frecuzrdgfunlem  10490  expclzaplem  10634  hashfiv01gt1  10853  wrdeq  10936  fsum2dlemstep  11577  fprod2dlemstep  11765  sin02gt0  11907  qredeu  12235  prmdc  12268  subrngrng  13698  lgslem3  15118  bj-stim  15238  bj-stan  15239  bj-stal  15241  bj-nfalt  15256  bj-indint  15423  tridceq  15546