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  850  stdcn  855  ifpdc  988  xordc1  1438  hbxfrbi  1521  nfalt  1627  19.29r  1670  19.31r  1729  sbimi  1812  spsbbi  1892  sbi2v  1941  euan  2136  2exeu  2172  ralimi2  2593  reximi2  2629  r19.28av  2670  r19.29r  2672  elex  2815  rmoan  3007  rmoimi2  3010  sseq2  3252  rabss2  3311  unssdif  3444  inssdif  3445  unssin  3448  inssun  3449  rabn0r  3523  undif4  3559  ssdif0im  3561  inssdif0im  3564  ssundifim  3580  ralf0  3599  prmg  3798  difprsnss  3816  snsspw  3852  pwprss  3894  pwtpss  3895  uniin  3918  intss  3954  iuniin  3985  iuneq1  3988  iuneq2  3991  iundif2ss  4041  iinuniss  4058  iunpwss  4067  intexrabim  4248  exmidundif  4302  exmidundifim  4303  exss  4325  pwunss  4386  soeq2  4419  ordunisuc2r  4618  peano5  4702  reliin  4855  coeq1  4893  coeq2  4894  cnveq  4910  dmeq  4937  dmin  4945  dmcoss  5008  rncoeq  5012  resiexg  5064  dminss  5158  imainss  5159  dfco2a  5244  euiotaex  5310  eliotaeu  5322  fundif  5381  fununi  5405  fof  5568  f1ocnv  5605  rexrnmpt  5798  isocnv  5962  isotr  5967  oprabid  6060  dmtpos  6465  tposfn  6482  smores  6501  eqer  6777  ixpeq2  6924  enssdom  6978  fiprc  7033  fiintim  7166  ltexprlemlol  7882  ltexprlemupu  7884  recexgt0  8819  peano2uz2  9648  eluzp1p1  9843  peano2uz  9878  zq  9921  ubmelfzo  10508  frecuzrdgtcl  10737  frecuzrdgfunlem  10744  expclzaplem  10888  hashfiv01gt1  11107  wrdeq  11201  fsum2dlemstep  12075  fprod2dlemstep  12263  sin02gt0  12405  qredeu  12749  prmdc  12782  subrngrng  14297  lgslem3  15821  clwwlkccat  16342  clwwlknonccat  16374  bj-stim  16464  bj-stan  16465  bj-stal  16467  bj-nfalt  16482  bj-indint  16647  tridceq  16789