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  659  pm2.67-2  714  oibabs  715  stdcn  848  pm2.85dc  906  peircedc  915  3jaob  1314  hbim  1567  hbimd  1595  i19.39  1662  hbae  1740  sbcof2  1832  sb4or  1855  tfi  4628  dmcosseq  4947  fliftfun  5855  tfrcl  6440  ac6sfi  6977  fsum2d  11665  fsumabs  11695  fsumiun  11707  fprod2d  11853  dvmptfsum  15115  bj-nnsn  15533  bj-pm2.18st  15550  setindis  15767  bdsetindis  15769