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  653  pm2.67-2  708  oibabs  709  stdcn  842  pm2.85dc  900  peircedc  909  3jaob  1297  hbim  1538  hbimd  1566  i19.39  1633  hbae  1711  sbcof2  1803  sb4or  1826  tfi  4566  dmcosseq  4882  fliftfun  5775  tfrcl  6343  ac6sfi  6876  fsum2d  11398  fsumabs  11428  fsumiun  11440  fprod2d  11586  bj-nnsn  13768  bj-pm2.18st  13785  setindis  14002  bdsetindis  14004