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  647  pm2.67-2  702  oibabs  703  stdcn  832  pm2.85dc  890  peircedc  899  3jaob  1280  hbim  1524  hbimd  1552  i19.39  1619  hbae  1696  sbcof2  1782  sb4or  1805  tfi  4496  dmcosseq  4810  fliftfun  5697  tfrcl  6261  ac6sfi  6792  fsum2d  11204  fsumabs  11234  fsumiun  11246  bj-nnsn  12945  bj-pm2.18st  12958  setindis  13165  bdsetindis  13167