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 ) )

This proof depends on syntax axioms:   -> wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used 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  4729  dmcosseq  5054  fliftfun  6002  tfrcl  6635  ac6sfi  7202  fsum2d  12202  fsumabs  12232  fsumiun  12244  fprod2d  12390  dvmptfsum  15826  bj-nnsn  16761  bj-pm2.18st  16778  setindis  16993  bdsetindis  16995