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  616  pm2.67-2  666  oibabs  833  pm2.85dc  844  peircedc  853  3jaob  1233  hbim  1477  hbimd  1505  i19.39  1571  hbae  1646  sbcof2  1731  sb4or  1754  tfi  4323  dmcosseq  4621  fliftfun  5456  ac6sfi  6379  setindis  10762  bdsetindis  10764