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  1383  hbxfrbi  1460  nfalt  1566  19.29r  1609  19.31r  1669  sbimi  1752  spsbbi  1832  sbi2v  1880  euan  2070  2exeu  2106  ralimi2  2526  reximi2  2562  r19.28av  2602  r19.29r  2604  elex  2737  rmoan  2926  rmoimi2  2929  sseq2  3166  rabss2  3225  unssdif  3357  inssdif  3358  unssin  3361  inssun  3362  rabn0r  3435  undif4  3471  ssdif0im  3473  inssdif0im  3476  ssundifim  3492  ralf0  3512  prmg  3697  difprsnss  3711  snsspw  3744  pwprss  3785  pwtpss  3786  uniin  3809  intss  3845  iuniin  3876  iuneq1  3879  iuneq2  3882  iundif2ss  3931  iinuniss  3948  iunpwss  3957  intexrabim  4132  exmidundif  4185  exmidundifim  4186  exss  4205  pwunss  4261  soeq2  4294  ordunisuc2r  4491  peano5  4575  reliin  4726  coeq1  4761  coeq2  4762  cnveq  4778  dmeq  4804  dmin  4812  dmcoss  4873  rncoeq  4877  resiexg  4929  dminss  5018  imainss  5019  dfco2a  5104  euiotaex  5169  fununi  5256  fof  5410  f1ocnv  5445  rexrnmpt  5628  isocnv  5779  isotr  5784  oprabid  5874  dmtpos  6224  tposfn  6241  smores  6260  eqer  6533  ixpeq2  6678  enssdom  6728  fiprc  6781  fiintim  6894  ltexprlemlol  7543  ltexprlemupu  7545  recexgt0  8478  peano2uz2  9298  eluzp1p1  9491  peano2uz  9521  zq  9564  ubmelfzo  10135  frecuzrdgtcl  10347  frecuzrdgfunlem  10354  expclzaplem  10479  hashfiv01gt1  10695  fsum2dlemstep  11375  fprod2dlemstep  11563  sin02gt0  11704  qredeu  12029  prmdc  12062  lgslem3  13543  bj-stim  13627  bj-stan  13628  bj-stal  13630  bj-nfalt  13645  bj-indint  13813  tridceq  13935