Theorem 3imtr4i 190

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

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

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  dcn  746  dcan  842  xordc1  1284  hbxfrbi  1361  nfalt  1470  19.29r  1512  19.31r  1571  sbimi  1647  spsbbi  1725  sbi2v  1772  euan  1956  2exeu  1992  ralimi2  2381  reximi2  2415  r19.28av  2449  r19.29r  2451  elex  2566  rmoan  2739  rmoimi2  2742  sseq2  2967  rabss2  3023  unssdif  3172  inssdif  3173  unssin  3176  inssun  3177  rabn0r  3244  undif4  3284  ssdif0im  3286  inssdif0im  3291  ssundifim  3306  ralf0  3324  prmg  3489  difprsnss  3502  snsspw  3535  pwprss  3576  pwtpss  3577  uniin  3600  intss  3636  iuniin  3667  iuneq1  3670  iuneq2  3673  iundif2ss  3722  iinuniss  3737  iunpwss  3743  intexrabim  3907  exss  3963  pwunss  4020  soeq2  4053  ordunisuc2r  4240  peano5  4321  reliin  4459  coeq1  4493  coeq2  4494  cnveq  4509  dmeq  4535  dmin  4543  dmcoss  4601  rncoeq  4605  resiexg  4653  dminss  4738  imainss  4739  dfco2a  4821  euiotaex  4883  fununi  4967  fof  5106  f1ocnv  5139  rexrnmpt  5310  isocnv  5451  isotr  5456  oprabid  5537  dmtpos  5871  tposfn  5888  smores  5907  eqer  6138  enssdom  6242  fiprc  6292  ltexprlemlol  6700  ltexprlemupu  6702  recexgt0  7571  peano2uz2  8345  eluzp1p1  8498  peano2uz  8526  zq  8561  elfzmlbmOLD  8989  ubmelfzo  9056  frecuzrdgfn  9198  expclzaplem  9279  bj-indint  10055  peano5setOLD  10065