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  2055  2exeu  2091  ralimi2  2492  reximi2  2528  r19.28av  2568  r19.29r  2570  elex  2697  rmoan  2884  rmoimi2  2887  sseq2  3121  rabss2  3180  unssdif  3311  inssdif  3312  unssin  3315  inssun  3316  rabn0r  3389  undif4  3425  ssdif0im  3427  inssdif0im  3430  ssundifim  3446  ralf0  3466  prmg  3644  difprsnss  3658  snsspw  3691  pwprss  3732  pwtpss  3733  uniin  3756  intss  3792  iuniin  3823  iuneq1  3826  iuneq2  3829  iundif2ss  3878  iinuniss  3895  iunpwss  3904  intexrabim  4078  exmidundif  4129  exmidundifim  4130  exss  4149  pwunss  4205  soeq2  4238  ordunisuc2r  4430  peano5  4512  reliin  4661  coeq1  4696  coeq2  4697  cnveq  4713  dmeq  4739  dmin  4747  dmcoss  4808  rncoeq  4812  resiexg  4864  dminss  4953  imainss  4954  dfco2a  5039  euiotaex  5104  fununi  5191  fof  5345  f1ocnv  5380  rexrnmpt  5563  isocnv  5712  isotr  5717  oprabid  5803  dmtpos  6153  tposfn  6170  smores  6189  eqer  6461  ixpeq2  6606  enssdom  6656  fiprc  6709  fiintim  6817  ltexprlemlol  7410  ltexprlemupu  7412  recexgt0  8342  peano2uz2  9158  eluzp1p1  9351  peano2uz  9378  zq  9418  ubmelfzo  9977  frecuzrdgtcl  10185  frecuzrdgfunlem  10192  expclzaplem  10317  hashfiv01gt1  10528  fsum2dlemstep  11203  sin02gt0  11470  qredeu  11778  bj-stim  12954  bj-stan  12955  bj-stal  12957  bj-nfalt  12971  bj-indint  13129