Theorem imim1i 54

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 53	1 ⊢ ((ψ → χ) → (φ → χ))

Syntax hints:   → wi 4

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7

This theorem is referenced by:  jarr  91  bi3ant  213  pm3.41  314  pm3.42  315  jarl  583  pm2.67-2  633  oibabs  799  pm2.85dc  810  peircedc  819  3jaob  1196  hbim  1434  hbimd  1462  i19.39  1528  hbae  1603  sbcof2  1688  sb4or  1711  tfi  4248  dmcosseq  4546  fliftfun  5379  setindis  9427  bdsetindis  9429