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  844  stdcn  849  xordc1  1413  hbxfrbi  1496  nfalt  1602  19.29r  1645  19.31r  1705  sbimi  1788  spsbbi  1868  sbi2v  1917  euan  2112  2exeu  2148  ralimi2  2568  reximi2  2604  r19.28av  2644  r19.29r  2646  elex  2788  rmoan  2980  rmoimi2  2983  sseq2  3225  rabss2  3284  unssdif  3416  inssdif  3417  unssin  3420  inssun  3421  rabn0r  3495  undif4  3531  ssdif0im  3533  inssdif0im  3536  ssundifim  3552  ralf0  3571  prmg  3765  difprsnss  3782  snsspw  3818  pwprss  3860  pwtpss  3861  uniin  3884  intss  3920  iuniin  3951  iuneq1  3954  iuneq2  3957  iundif2ss  4007  iinuniss  4024  iunpwss  4033  intexrabim  4213  exmidundif  4266  exmidundifim  4267  exss  4289  pwunss  4348  soeq2  4381  ordunisuc2r  4580  peano5  4664  reliin  4815  coeq1  4853  coeq2  4854  cnveq  4870  dmeq  4897  dmin  4905  dmcoss  4967  rncoeq  4971  resiexg  5023  dminss  5116  imainss  5117  dfco2a  5202  euiotaex  5267  eliotaeu  5279  fundif  5337  fununi  5361  fof  5520  f1ocnv  5557  rexrnmpt  5746  isocnv  5903  isotr  5908  oprabid  5999  dmtpos  6365  tposfn  6382  smores  6401  eqer  6675  ixpeq2  6822  enssdom  6876  fiprc  6931  fiintim  7054  ltexprlemlol  7750  ltexprlemupu  7752  recexgt0  8688  peano2uz2  9515  eluzp1p1  9709  peano2uz  9739  zq  9782  ubmelfzo  10366  frecuzrdgtcl  10594  frecuzrdgfunlem  10601  expclzaplem  10745  hashfiv01gt1  10964  wrdeq  11053  fsum2dlemstep  11860  fprod2dlemstep  12048  sin02gt0  12190  qredeu  12534  prmdc  12567  subrngrng  14079  lgslem3  15594  bj-stim  15882  bj-stan  15883  bj-stal  15885  bj-nfalt  15900  bj-indint  16066  tridceq  16197