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  647  pm2.67-2  702  oibabs  703  stdcn  832  pm2.85dc  890  peircedc  899  3jaob  1280  hbim  1524  hbimd  1552  i19.39  1619  hbae  1696  sbcof2  1782  sb4or  1805  tfi  4491  dmcosseq  4805  fliftfun  5690  tfrcl  6254  ac6sfi  6785  fsum2d  11197  fsumabs  11227  fsumiun  11239  bj-nnsn  12934  bj-pm2.18st  12947  setindis  13154  bdsetindis  13156