Theorem imim1i 60

Description: Inference adding common consequents in an implication, thereby interchanging the original antecedent and consequent. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 4-Aug-2012.)

Hypothesis

Ref	Expression
imim1i.1	|- ( ph -> ps )

Assertion

Ref	Expression
imim1i	|- ( ( ps -> ch ) -> ( ph -> ch ) )

Proof of Theorem imim1i

Step	Hyp	Ref	Expression
1		imim1i.1	. 2 |- ( ph -> ps )
2		id 19	. 2 |- ( ch -> ch )
3	1, 2	imim12i 59	1 |- ( ( ps -> ch ) -> ( ph -> ch ) )

Syntax hints:   -> wi 4

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

This theorem is referenced by:  jarr  97  bi3ant  224  pm3.41  331  pm3.42  332  jarl  668  pm2.67-2  725  oibabs  726  stdcn  859  pm2.85dc  917  peircedc  926  3jaob  1343  hbim  1598  hbimd  1626  i19.39  1693  hbae  1770  sbcof2  1863  sb4or  1886  tfi  4724  dmcosseq  5049  fliftfun  5992  tfrcl  6625  ac6sfi  7192  fsum2d  12180  fsumabs  12210  fsumiun  12222  fprod2d  12368  dvmptfsum  15749  bj-nnsn  16675  bj-pm2.18st  16692  setindis  16907  bdsetindis  16909