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  664  pm2.67-2  720  oibabs  721  stdcn  854  pm2.85dc  912  peircedc  921  3jaob  1338  hbim  1593  hbimd  1621  i19.39  1688  hbae  1766  sbcof2  1858  sb4or  1881  tfi  4680  dmcosseq  5004  fliftfun  5936  tfrcl  6529  ac6sfi  7086  fsum2d  11995  fsumabs  12025  fsumiun  12037  fprod2d  12183  dvmptfsum  15448  bj-nnsn  16329  bj-pm2.18st  16346  setindis  16562  bdsetindis  16564