Theorem 3imtr4i 200

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

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

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  dcn  827  stdcn  832  dcan  918  xordc1  1371  hbxfrbi  1448  nfalt  1557  19.29r  1600  19.31r  1659  sbimi  1737  spsbbi  1816  sbi2v  1864  euan  2053  2exeu  2089  ralimi2  2490  reximi2  2526  r19.28av  2566  r19.29r  2568  elex  2692  rmoan  2879  rmoimi2  2882  sseq2  3116  rabss2  3175  unssdif  3306  inssdif  3307  unssin  3310  inssun  3311  rabn0r  3384  undif4  3420  ssdif0im  3422  inssdif0im  3425  ssundifim  3441  ralf0  3461  prmg  3639  difprsnss  3653  snsspw  3686  pwprss  3727  pwtpss  3728  uniin  3751  intss  3787  iuniin  3818  iuneq1  3821  iuneq2  3824  iundif2ss  3873  iinuniss  3890  iunpwss  3899  intexrabim  4073  exmidundif  4124  exmidundifim  4125  exss  4144  pwunss  4200  soeq2  4233  ordunisuc2r  4425  peano5  4507  reliin  4656  coeq1  4691  coeq2  4692  cnveq  4708  dmeq  4734  dmin  4742  dmcoss  4803  rncoeq  4807  resiexg  4859  dminss  4948  imainss  4949  dfco2a  5034  euiotaex  5099  fununi  5186  fof  5340  f1ocnv  5373  rexrnmpt  5556  isocnv  5705  isotr  5710  oprabid  5796  dmtpos  6146  tposfn  6163  smores  6182  eqer  6454  ixpeq2  6599  enssdom  6649  fiprc  6702  fiintim  6810  ltexprlemlol  7403  ltexprlemupu  7405  recexgt0  8335  peano2uz2  9151  eluzp1p1  9344  peano2uz  9371  zq  9411  ubmelfzo  9970  frecuzrdgtcl  10178  frecuzrdgfunlem  10185  expclzaplem  10310  hashfiv01gt1  10521  fsum2dlemstep  11196  sin02gt0  11459  qredeu  11767  bj-stim  12943  bj-stan  12944  bj-stal  12946  bj-nfalt  12960  bj-indint  13118