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  779  dcan  875  xordc1  1324  hbxfrbi  1401  nfalt  1510  19.29r  1552  19.31r  1611  sbimi  1687  spsbbi  1765  sbi2v  1813  euan  1997  2exeu  2033  ralimi2  2423  reximi2  2457  r19.28av  2493  r19.29r  2495  elex  2610  rmoan  2790  rmoimi2  2793  sseq2  3021  rabss2  3077  unssdif  3199  inssdif  3200  unssin  3203  inssun  3204  rabn0r  3271  undif4  3306  ssdif0im  3308  inssdif0im  3311  ssundifim  3326  ralf0  3344  prmg  3511  difprsnss  3524  snsspw  3556  pwprss  3597  pwtpss  3598  uniin  3621  intss  3657  iuniin  3688  iuneq1  3691  iuneq2  3694  iundif2ss  3743  iinuniss  3758  iunpwss  3764  intexrabim  3928  exss  3982  pwunss  4038  soeq2  4071  ordunisuc2r  4258  peano5  4339  reliin  4477  coeq1  4511  coeq2  4512  cnveq  4527  dmeq  4553  dmin  4561  dmcoss  4619  rncoeq  4623  resiexg  4673  dminss  4758  imainss  4759  dfco2a  4841  euiotaex  4903  fununi  4987  fof  5126  f1ocnv  5159  rexrnmpt  5331  isocnv  5471  isotr  5476  oprabid  5557  dmtpos  5894  tposfn  5911  smores  5930  eqer  6161  enssdom  6265  fiprc  6315  ltexprlemlol  6792  ltexprlemupu  6794  recexgt0  7680  peano2uz2  8454  eluzp1p1  8644  peano2uz  8671  zq  8711  ubmelfzo  9209  frecuzrdgfn  9414  expclzaplem  9500  qredeu  10479  bj-indint  10726