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  648  pm2.67-2  703  oibabs  704  stdcn  833  pm2.85dc  891  peircedc  900  3jaob  1281  hbim  1525  hbimd  1553  i19.39  1620  hbae  1697  sbcof2  1783  sb4or  1806  tfi  4504  dmcosseq  4818  fliftfun  5705  tfrcl  6269  ac6sfi  6800  fsum2d  11236  fsumabs  11266  fsumiun  11278  bj-nnsn  13116  bj-pm2.18st  13129  setindis  13336  bdsetindis  13338