Theorem 3imtr4i 257

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 177

This theorem is referenced by:  hbxfrbi  1568  19.30  1604  sbimi  1652  hba1  1786  nfimdOLD  1809  euan  2261  ralimi2  2687  reximi2  2721  r19.28av  2754  r19.29r  2756  r19.30  2757  elex  2868  rmoan  3035  rmoimi2  3038  sseq2  3294  rabss2  3350  undif4  3608  r19.2zb  3641  ralf0  3657  difprsnss  3847  snsspw  3878  uniin  3912  intss  3948  iuniin  3980  iuneq1  3983  iuneq2  3986  iunpwss  4056  iotaex  4357  peano2  4404  nnpw1ex  4485  spfininduct  4541  brex  4690  coeq1  4875  coeq2  4876  cnveq  4887  dmeq  4908  dmin  4914  brelrn  4961  dmcoss  4972  rncoeq  4976  dminss  5042  imainss  5043  dfco2a  5082  funmo  5126  funeq  5128  funun  5147  fununi  5161  2elresin  5195  fco  5232  f1co  5265  fof  5270  foco  5280  f1ores  5301  f1oco  5309  fvpr2  5451  isocnv  5492  isotr  5496  oprabid  5551  fntxp  5805  fnpprod  5844  f1opprod  5845  ider  5944  ssetpov  5945  eqer  5962  map0  6026  unen  6049  pw1fin  6170  cenc  6182  lecidg  6197  lec0cg  6199  lecncvg  6200  sbth  6207  addlec  6209  nc0le1  6217  ce2le  6234  dmfrec  6317  scancan  6332