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  842  stdcn  847  dcan  933  xordc1  1393  hbxfrbi  1472  nfalt  1578  19.29r  1621  19.31r  1681  sbimi  1764  spsbbi  1844  sbi2v  1892  euan  2082  2exeu  2118  ralimi2  2537  reximi2  2573  r19.28av  2613  r19.29r  2615  elex  2750  rmoan  2939  rmoimi2  2942  sseq2  3181  rabss2  3240  unssdif  3372  inssdif  3373  unssin  3376  inssun  3377  rabn0r  3451  undif4  3487  ssdif0im  3489  inssdif0im  3492  ssundifim  3508  ralf0  3528  prmg  3715  difprsnss  3732  snsspw  3766  pwprss  3807  pwtpss  3808  uniin  3831  intss  3867  iuniin  3898  iuneq1  3901  iuneq2  3904  iundif2ss  3954  iinuniss  3971  iunpwss  3980  intexrabim  4155  exmidundif  4208  exmidundifim  4209  exss  4229  pwunss  4285  soeq2  4318  ordunisuc2r  4515  peano5  4599  reliin  4750  coeq1  4786  coeq2  4787  cnveq  4803  dmeq  4829  dmin  4837  dmcoss  4898  rncoeq  4902  resiexg  4954  dminss  5045  imainss  5046  dfco2a  5131  euiotaex  5196  eliotaeu  5207  fununi  5286  fof  5440  f1ocnv  5476  rexrnmpt  5661  isocnv  5814  isotr  5819  oprabid  5909  dmtpos  6259  tposfn  6276  smores  6295  eqer  6569  ixpeq2  6714  enssdom  6764  fiprc  6817  fiintim  6930  ltexprlemlol  7603  ltexprlemupu  7605  recexgt0  8539  peano2uz2  9362  eluzp1p1  9555  peano2uz  9585  zq  9628  ubmelfzo  10202  frecuzrdgtcl  10414  frecuzrdgfunlem  10421  expclzaplem  10546  hashfiv01gt1  10764  fsum2dlemstep  11444  fprod2dlemstep  11632  sin02gt0  11773  qredeu  12099  prmdc  12132  lgslem3  14488  bj-stim  14583  bj-stan  14584  bj-stal  14586  bj-nfalt  14601  bj-indint  14768  tridceq  14889