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  568  pm2.67-2  618  oibabs  784  pm2.85dc  795  peircedc  804  3jaob  1178  hbim  1410  hbimd  1438  i19.39  1504  hbae  1579  sbcof2  1664  sb4or  1687  tfi  4220  dmcosseq  4518  fliftfun  5349  setindis  8347  bdsetindis  8349