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-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  dcn  810  stdcn  815  dcan  899  xordc1  1352  hbxfrbi  1429  nfalt  1538  19.29r  1581  19.31r  1640  sbimi  1718  spsbbi  1796  sbi2v  1844  euan  2029  2exeu  2065  ralimi2  2464  reximi2  2500  r19.28av  2540  r19.29r  2542  elex  2666  rmoan  2851  rmoimi2  2854  sseq2  3085  rabss2  3144  unssdif  3275  inssdif  3276  unssin  3279  inssun  3280  rabn0r  3353  undif4  3389  ssdif0im  3391  inssdif0im  3394  ssundifim  3410  ralf0  3430  prmg  3608  difprsnss  3622  snsspw  3655  pwprss  3696  pwtpss  3697  uniin  3720  intss  3756  iuniin  3787  iuneq1  3790  iuneq2  3793  iundif2ss  3842  iinuniss  3859  iunpwss  3868  intexrabim  4036  exmidundif  4087  exmidundifim  4088  exss  4107  pwunss  4163  soeq2  4196  ordunisuc2r  4388  peano5  4470  reliin  4619  coeq1  4654  coeq2  4655  cnveq  4671  dmeq  4697  dmin  4705  dmcoss  4764  rncoeq  4768  resiexg  4820  dminss  4909  imainss  4910  dfco2a  4995  euiotaex  5060  fununi  5147  fof  5301  f1ocnv  5334  rexrnmpt  5515  isocnv  5664  isotr  5669  oprabid  5755  dmtpos  6105  tposfn  6122  smores  6141  eqer  6413  ixpeq2  6558  enssdom  6608  fiprc  6661  fiintim  6768  ltexprlemlol  7352  ltexprlemupu  7354  recexgt0  8254  peano2uz2  9056  eluzp1p1  9247  peano2uz  9274  zq  9314  ubmelfzo  9864  frecuzrdgtcl  10072  frecuzrdgfunlem  10079  expclzaplem  10204  hashfiv01gt1  10415  fsum2dlemstep  11089  sin02gt0  11315  qredeu  11618  bj-stim  12637  bj-stan  12638  bj-stal  12640  bj-nfalt  12655  bj-indint  12812