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  660  pm2.67-2  715  oibabs  716  stdcn  849  pm2.85dc  907  peircedc  916  3jaob  1315  hbim  1569  hbimd  1597  i19.39  1664  hbae  1742  sbcof2  1834  sb4or  1857  tfi  4638  dmcosseq  4959  fliftfun  5878  tfrcl  6463  ac6sfi  7010  fsum2d  11821  fsumabs  11851  fsumiun  11863  fprod2d  12009  dvmptfsum  15272  bj-nnsn  15808  bj-pm2.18st  15825  setindis  16041  bdsetindis  16043