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  223  pm3.41  329  pm3.42  330  jarl  648  pm2.67-2  703  oibabs  704  stdcn  833  pm2.85dc  891  peircedc  900  3jaob  1284  hbim  1525  hbimd  1553  i19.39  1620  hbae  1698  sbcof2  1790  sb4or  1813  tfi  4542  dmcosseq  4858  fliftfun  5747  tfrcl  6312  ac6sfi  6844  fsum2d  11336  fsumabs  11366  fsumiun  11378  fprod2d  11524  bj-nnsn  13351  bj-pm2.18st  13365  setindis  13584  bdsetindis  13586