Theorem imim1i 59

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 58	1 |- ( ( ps -> ch ) -> ( ph -> ch ) )

Syntax hints:   -> wi 4

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7

This theorem is referenced by:  jarr  96  bi3ant  222  pm3.41  324  pm3.42  325  jarl  617  pm2.67-2  667  oibabs  834  pm2.85dc  845  peircedc  854  3jaob  1234  hbim  1478  hbimd  1506  i19.39  1572  hbae  1647  sbcof2  1732  sb4or  1755  tfi  4331  dmcosseq  4631  fliftfun  5467  tfrcl  6013  ac6sfi  6431  setindis  10920  bdsetindis  10922