Theorem 3imtr4i 201

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

This proof depends on syntax axioms:   -> wi 4   <-> wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  dcn  854  stdcn  859  ifpdc  992  xordc1  1442  hbxfrbi  1525  nfalt  1631  19.29r  1674  19.31r  1733  sbimi  1817  spsbbi  1897  sbi2v  1947  euan  2143  2exeu  2179  ralimi2  2610  reximi2  2646  r19.28av  2687  r19.29r  2689  elex  2833  rmoan  3026  rmoimi2  3029  sseq2  3272  rabss2  3331  unssdif  3466  inssdif  3467  unssin  3470  inssun  3471  rabn0r  3548  undif4  3587  ssdif0im  3589  inssdif0imOLD  3593  ssundifim  3611  ralf0  3630  prmg  3835  difprsnss  3853  snsspw  3889  pwprss  3931  pwtpss  3932  uniin  3955  intss  3991  iuniin  4022  iuneq1  4025  iuneq2  4028  iundif2ss  4078  iinuniss  4095  iunpwss  4104  intexrabim  4291  exmidundif  4345  exmidundifim  4346  exss  4369  pwunss  4430  soeq2  4463  ordunisuc2r  4663  peano5  4747  reliin  4901  coeq1  4939  coeq2  4940  cnveq  4956  dmeq  4983  dmin  4991  dmcoss  5054  rncoeq  5058  resiexg  5111  dminss  5205  imainss  5206  dfco2a  5291  euiotaex  5357  eliotaeu  5369  fundif  5428  fununi  5452  fof  5618  f1ocnv  5655  rexrnmpt  5854  isocnv  6020  isotr  6025  oprabid  6120  dmtpos  6531  tposfn  6548  smores  6567  eqer  6843  fsetsspwxp  6952  ixpeq2  6998  enssdom  7052  fiprc  7108  fiintim  7242  ltexprlemlol  7975  ltexprlemupu  7977  recexgt0  8916  peano2uz2  9764  eluzp1p1  9964  peano2uz  9999  zq  10042  ubmelfzo  10635  frecuzrdgtcl  10870  frecuzrdgfunlem  10877  expclzaplem  11021  hashfiv01gt1  11243  hashfibclem  11304  wrdeq  11348  fsum2dlemstep  12226  fprod2dlemstep  12414  sin02gt0  12556  qredeu  12900  prmdc  12933  ballotfilemth  13339  subrngrng  14619  lgslem3  16326  clwwlkccat  16847  clwwlknonccat  16879  bj-stim  16979  bj-stan  16980  bj-stal  16982  bj-nfalt  16997  bj-indint  17162  tridceq  17313  alseuals  17372  ralseurals  17373