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  658  pm2.67-2  713  oibabs  714  stdcn  847  pm2.85dc  905  peircedc  914  3jaob  1302  hbim  1545  hbimd  1573  i19.39  1640  hbae  1718  sbcof2  1810  sb4or  1833  tfi  4582  dmcosseq  4899  fliftfun  5797  tfrcl  6365  ac6sfi  6898  fsum2d  11443  fsumabs  11473  fsumiun  11485  fprod2d  11631  bj-nnsn  14488  bj-pm2.18st  14505  setindis  14722  bdsetindis  14724