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  224  pm3.41  331  pm3.42  332  jarl  664  pm2.67-2  720  oibabs  721  stdcn  854  pm2.85dc  912  peircedc  921  3jaob  1338  hbim  1593  hbimd  1621  i19.39  1688  hbae  1766  sbcof2  1858  sb4or  1881  tfi  4680  dmcosseq  5004  fliftfun  5937  tfrcl  6530  ac6sfi  7087  fsum2d  12014  fsumabs  12044  fsumiun  12056  fprod2d  12202  dvmptfsum  15468  bj-nnsn  16380  bj-pm2.18st  16397  setindis  16613  bdsetindis  16615