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  4731  dmcosseq  5056  fliftfun  6005  tfrcl  6639  ac6sfi  7206  fsum2d  12227  fsumabs  12257  fsumiun  12269  fprod2d  12415  dvmptfsum  15951  bj-nnsn  16966  bj-pm2.18st  16983  setindis  17198  bdsetindis  17200