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  832  stdcn  837  dcan  923  xordc1  1382  hbxfrbi  1459  nfalt  1565  19.29r  1608  19.31r  1668  sbimi  1751  spsbbi  1831  sbi2v  1879  euan  2069  2exeu  2105  ralimi2  2524  reximi2  2560  r19.28av  2600  r19.29r  2602  elex  2732  rmoan  2921  rmoimi2  2924  sseq2  3161  rabss2  3220  unssdif  3352  inssdif  3353  unssin  3356  inssun  3357  rabn0r  3430  undif4  3466  ssdif0im  3468  inssdif0im  3471  ssundifim  3487  ralf0  3507  prmg  3691  difprsnss  3705  snsspw  3738  pwprss  3779  pwtpss  3780  uniin  3803  intss  3839  iuniin  3870  iuneq1  3873  iuneq2  3876  iundif2ss  3925  iinuniss  3942  iunpwss  3951  intexrabim  4126  exmidundif  4179  exmidundifim  4180  exss  4199  pwunss  4255  soeq2  4288  ordunisuc2r  4485  peano5  4569  reliin  4720  coeq1  4755  coeq2  4756  cnveq  4772  dmeq  4798  dmin  4806  dmcoss  4867  rncoeq  4871  resiexg  4923  dminss  5012  imainss  5013  dfco2a  5098  euiotaex  5163  fununi  5250  fof  5404  f1ocnv  5439  rexrnmpt  5622  isocnv  5773  isotr  5778  oprabid  5865  dmtpos  6215  tposfn  6232  smores  6251  eqer  6524  ixpeq2  6669  enssdom  6719  fiprc  6772  fiintim  6885  ltexprlemlol  7534  ltexprlemupu  7536  recexgt0  8469  peano2uz2  9289  eluzp1p1  9482  peano2uz  9512  zq  9555  ubmelfzo  10125  frecuzrdgtcl  10337  frecuzrdgfunlem  10344  expclzaplem  10469  hashfiv01gt1  10684  fsum2dlemstep  11361  fprod2dlemstep  11549  sin02gt0  11690  qredeu  12008  prmdc  12041  bj-stim  13461  bj-stan  13462  bj-stal  13464  bj-nfalt  13480  bj-indint  13648  tridceq  13769