Theorem 3imtr4i 199

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 119	. 2 |- ( ch -> ps )
4		3imtr4.3	. 2 |- ( th <-> ps )
5	3, 4	sylibr 132	1 |- ( ch -> th )

Syntax hints:   -> wi 4   <-> wb 103

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  dcn  780  dcan  876  xordc1  1325  hbxfrbi  1402  nfalt  1511  19.29r  1553  19.31r  1612  sbimi  1688  spsbbi  1766  sbi2v  1814  euan  1998  2exeu  2034  ralimi2  2424  reximi2  2458  r19.28av  2494  r19.29r  2496  elex  2611  rmoan  2791  rmoimi2  2794  sseq2  3022  rabss2  3078  unssdif  3206  inssdif  3207  unssin  3210  inssun  3211  rabn0r  3278  undif4  3313  ssdif0im  3315  inssdif0im  3318  ssundifim  3333  ralf0  3352  prmg  3519  difprsnss  3532  snsspw  3564  pwprss  3605  pwtpss  3606  uniin  3629  intss  3665  iuniin  3696  iuneq1  3699  iuneq2  3702  iundif2ss  3751  iinuniss  3766  iunpwss  3772  intexrabim  3936  exss  3990  pwunss  4046  soeq2  4079  ordunisuc2r  4266  peano5  4347  reliin  4487  coeq1  4521  coeq2  4522  cnveq  4537  dmeq  4563  dmin  4571  dmcoss  4629  rncoeq  4633  resiexg  4683  dminss  4768  imainss  4769  dfco2a  4851  euiotaex  4913  fununi  4998  fof  5137  f1ocnv  5170  rexrnmpt  5342  isocnv  5482  isotr  5487  oprabid  5568  dmtpos  5905  tposfn  5922  smores  5941  eqer  6204  enssdom  6309  fiprc  6360  ltexprlemlol  6854  ltexprlemupu  6856  recexgt0  7747  peano2uz2  8535  eluzp1p1  8725  peano2uz  8752  zq  8792  ubmelfzo  9286  frecuzrdgtcl  9494  frecuzrdgfunlem  9501  expclzaplem  9597  sizefiv01gt1  9806  qredeu  10623  bj-indint  10884