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  3441  undif4  3477  ssdif0im  3479  inssdif0im  3482  ssundifim  3498  ralf0  3518  prmg  3704  difprsnss  3718  snsspw  3751  pwprss  3792  pwtpss  3793  uniin  3816  intss  3852  iuniin  3883  iuneq1  3886  iuneq2  3889  iundif2ss  3938  iinuniss  3955  iunpwss  3964  intexrabim  4139  exmidundif  4192  exmidundifim  4193  exss  4212  pwunss  4268  soeq2  4301  ordunisuc2r  4498  peano5  4582  reliin  4733  coeq1  4768  coeq2  4769  cnveq  4785  dmeq  4811  dmin  4819  dmcoss  4880  rncoeq  4884  resiexg  4936  dminss  5025  imainss  5026  dfco2a  5111  euiotaex  5176  eliotaeu  5187  fununi  5266  fof  5420  f1ocnv  5455  rexrnmpt  5639  isocnv  5790  isotr  5795  oprabid  5885  dmtpos  6235  tposfn  6252  smores  6271  eqer  6545  ixpeq2  6690  enssdom  6740  fiprc  6793  fiintim  6906  ltexprlemlol  7564  ltexprlemupu  7566  recexgt0  8499  peano2uz2  9319  eluzp1p1  9512  peano2uz  9542  zq  9585  ubmelfzo  10156  frecuzrdgtcl  10368  frecuzrdgfunlem  10375  expclzaplem  10500  hashfiv01gt1  10716  fsum2dlemstep  11397  fprod2dlemstep  11585  sin02gt0  11726  qredeu  12051  prmdc  12084  lgslem3  13697  bj-stim  13781  bj-stan  13782  bj-stal  13784  bj-nfalt  13799  bj-indint  13966  tridceq  14088