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  721  oibabs  722  stdcn  855  pm2.85dc  913  peircedc  922  3jaob  1339  hbim  1594  hbimd  1622  i19.39  1689  hbae  1766  sbcof2  1858  sb4or  1881  tfi  4686  dmcosseq  5010  fliftfun  5947  tfrcl  6573  ac6sfi  7130  fsum2d  12059  fsumabs  12089  fsumiun  12101  fprod2d  12247  dvmptfsum  15519  bj-nnsn  16434  bj-pm2.18st  16451  setindis  16666  bdsetindis  16668