Theorem 3imtr4i 200

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 120	. 2 |- ( ch -> ps )
4		3imtr4.3	. 2 |- ( th <-> ps )
5	3, 4	sylibr 133	1 |- ( ch -> th )

Syntax hints:   -> wi 4   <-> wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  dcn  837  stdcn  842  dcan  928  xordc1  1388  hbxfrbi  1465  nfalt  1571  19.29r  1614  19.31r  1674  sbimi  1757  spsbbi  1837  sbi2v  1885  euan  2075  2exeu  2111  ralimi2  2530  reximi2  2566  r19.28av  2606  r19.29r  2608  elex  2741  rmoan  2930  rmoimi2  2933  sseq2  3171  rabss2  3230  unssdif  3362  inssdif  3363  unssin  3366  inssun  3367  rabn0r  3440  undif4  3476  ssdif0im  3478  inssdif0im  3481  ssundifim  3497  ralf0  3517  prmg  3702  difprsnss  3716  snsspw  3749  pwprss  3790  pwtpss  3791  uniin  3814  intss  3850  iuniin  3881  iuneq1  3884  iuneq2  3887  iundif2ss  3936  iinuniss  3953  iunpwss  3962  intexrabim  4137  exmidundif  4190  exmidundifim  4191  exss  4210  pwunss  4266  soeq2  4299  ordunisuc2r  4496  peano5  4580  reliin  4731  coeq1  4766  coeq2  4767  cnveq  4783  dmeq  4809  dmin  4817  dmcoss  4878  rncoeq  4882  resiexg  4934  dminss  5023  imainss  5024  dfco2a  5109  euiotaex  5174  eliotaeu  5185  fununi  5264  fof  5418  f1ocnv  5453  rexrnmpt  5636  isocnv  5787  isotr  5792  oprabid  5882  dmtpos  6232  tposfn  6249  smores  6268  eqer  6541  ixpeq2  6686  enssdom  6736  fiprc  6789  fiintim  6902  ltexprlemlol  7551  ltexprlemupu  7553  recexgt0  8486  peano2uz2  9306  eluzp1p1  9499  peano2uz  9529  zq  9572  ubmelfzo  10143  frecuzrdgtcl  10355  frecuzrdgfunlem  10362  expclzaplem  10487  hashfiv01gt1  10703  fsum2dlemstep  11384  fprod2dlemstep  11572  sin02gt0  11713  qredeu  12038  prmdc  12071  lgslem3  13656  bj-stim  13740  bj-stan  13741  bj-stal  13743  bj-nfalt  13758  bj-indint  13926  tridceq  14048