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  854  stdcn  859  ifpdc  992  xordc1  1442  hbxfrbi  1525  nfalt  1631  19.29r  1674  19.31r  1733  sbimi  1817  spsbbi  1897  sbi2v  1947  euan  2143  2exeu  2179  ralimi2  2610  reximi2  2646  r19.28av  2687  r19.29r  2689  elex  2833  rmoan  3026  rmoimi2  3029  sseq2  3272  rabss2  3331  unssdif  3466  inssdif  3467  unssin  3470  inssun  3471  rabn0r  3548  undif4  3587  ssdif0im  3589  inssdif0imOLD  3593  ssundifim  3611  ralf0  3630  prmg  3833  difprsnss  3851  snsspw  3887  pwprss  3929  pwtpss  3930  uniin  3953  intss  3989  iuniin  4020  iuneq1  4023  iuneq2  4026  iundif2ss  4076  iinuniss  4093  iunpwss  4102  intexrabim  4287  exmidundif  4341  exmidundifim  4342  exss  4365  pwunss  4426  soeq2  4459  ordunisuc2r  4659  peano5  4743  reliin  4897  coeq1  4935  coeq2  4936  cnveq  4952  dmeq  4979  dmin  4987  dmcoss  5050  rncoeq  5054  resiexg  5106  dminss  5200  imainss  5201  dfco2a  5286  euiotaex  5352  eliotaeu  5364  fundif  5423  fununi  5447  fof  5613  f1ocnv  5650  rexrnmpt  5845  isocnv  6010  isotr  6015  oprabid  6110  dmtpos  6520  tposfn  6537  smores  6556  eqer  6832  fsetsspwxp  6941  ixpeq2  6987  enssdom  7041  fiprc  7097  fiintim  7231  ltexprlemlol  7962  ltexprlemupu  7964  recexgt0  8901  peano2uz2  9735  eluzp1p1  9930  peano2uz  9965  zq  10008  ubmelfzo  10599  frecuzrdgtcl  10830  frecuzrdgfunlem  10837  expclzaplem  10981  hashfiv01gt1  11202  hashfibclem  11263  wrdeq  11307  fsum2dlemstep  12182  fprod2dlemstep  12370  sin02gt0  12512  qredeu  12856  prmdc  12889  ballotfilemth  13262  subrngrng  14486  lgslem3  16038  clwwlkccat  16559  clwwlknonccat  16591  bj-stim  16691  bj-stan  16692  bj-stal  16694  bj-nfalt  16709  bj-indint  16874  tridceq  17014