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	⊢ (𝜑 → 𝜓)

Assertion

Ref	Expression
imim1i	⊢ ((𝜓 → 𝜒) → (𝜑 → 𝜒))

Proof of Theorem imim1i

Step	Hyp	Ref	Expression
1		imim1i.1	. 2 ⊢ (𝜑 → 𝜓)
2		id 19	. 2 ⊢ (𝜒 → 𝜒)
3	1, 2	imim12i 59	1 ⊢ ((𝜓 → 𝜒) → (𝜑 → 𝜒))

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  662  pm2.67-2  718  oibabs  719  stdcn  852  pm2.85dc  910  peircedc  919  3jaob  1336  hbim  1591  hbimd  1619  i19.39  1686  hbae  1764  sbcof2  1856  sb4or  1879  tfi  4676  dmcosseq  5000  fliftfun  5930  tfrcl  6523  ac6sfi  7078  fsum2d  11983  fsumabs  12013  fsumiun  12025  fprod2d  12171  dvmptfsum  15436  bj-nnsn  16239  bj-pm2.18st  16256  setindis  16472  bdsetindis  16474