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  1486  nfalt  1592  19.29r  1635  19.31r  1695  sbimi  1778  spsbbi  1858  sbi2v  1907  euan  2101  2exeu  2137  ralimi2  2557  reximi2  2593  r19.28av  2633  r19.29r  2635  elex  2774  rmoan  2964  rmoimi2  2967  sseq2  3208  rabss2  3267  unssdif  3399  inssdif  3400  unssin  3403  inssun  3404  rabn0r  3478  undif4  3514  ssdif0im  3516  inssdif0im  3519  ssundifim  3535  ralf0  3554  prmg  3744  difprsnss  3761  snsspw  3795  pwprss  3836  pwtpss  3837  uniin  3860  intss  3896  iuniin  3927  iuneq1  3930  iuneq2  3933  iundif2ss  3983  iinuniss  4000  iunpwss  4009  intexrabim  4187  exmidundif  4240  exmidundifim  4241  exss  4261  pwunss  4319  soeq2  4352  ordunisuc2r  4551  peano5  4635  reliin  4786  coeq1  4824  coeq2  4825  cnveq  4841  dmeq  4867  dmin  4875  dmcoss  4936  rncoeq  4940  resiexg  4992  dminss  5085  imainss  5086  dfco2a  5171  euiotaex  5236  eliotaeu  5248  fununi  5327  fof  5483  f1ocnv  5520  rexrnmpt  5708  isocnv  5861  isotr  5866  oprabid  5957  dmtpos  6323  tposfn  6340  smores  6359  eqer  6633  ixpeq2  6780  enssdom  6830  fiprc  6883  fiintim  7001  ltexprlemlol  7686  ltexprlemupu  7688  recexgt0  8624  peano2uz2  9450  eluzp1p1  9644  peano2uz  9674  zq  9717  ubmelfzo  10293  frecuzrdgtcl  10521  frecuzrdgfunlem  10528  expclzaplem  10672  hashfiv01gt1  10891  wrdeq  10974  fsum2dlemstep  11616  fprod2dlemstep  11804  sin02gt0  11946  qredeu  12290  prmdc  12323  subrngrng  13834  lgslem3  15327  bj-stim  15476  bj-stan  15477  bj-stal  15479  bj-nfalt  15494  bj-indint  15661  tridceq  15787