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  223  pm3.41  329  pm3.42  330  jarl  648  pm2.67-2  703  oibabs  704  stdcn  837  pm2.85dc  895  peircedc  904  3jaob  1292  hbim  1533  hbimd  1561  i19.39  1628  hbae  1706  sbcof2  1798  sb4or  1821  tfi  4559  dmcosseq  4875  fliftfun  5764  tfrcl  6332  ac6sfi  6864  fsum2d  11376  fsumabs  11406  fsumiun  11418  fprod2d  11564  bj-nnsn  13614  bj-pm2.18st  13631  setindis  13849  bdsetindis  13851