Theorem ja 137

Description: Inference joining the antecedents of two premises. (The proof was shortened by O'Cat, 19-Feb-2008.)

Hypotheses

Ref	Expression
ja.1	⊢ (¬ φ → χ)
ja.2	⊢ (ψ → χ)

Assertion

Ref	Expression
ja	⊢ ((φ → ψ) → χ)

Proof of Theorem ja

Step	Hyp	Ref	Expression
1		ja.2	. . 3 ⊢ (ψ → χ)
2	1	imim2i 17	. 2 ⊢ ((φ → ψ) → (φ → χ))
3		ja.1	. 2 ⊢ (¬ φ → χ)
4	2, 3	pm2.61d1 128	1 ⊢ ((φ → ψ) → χ)

Syntax hints:  ¬ wn 2   → wi 3

This theorem is referenced by:  pm2.74 575  pm5.71 750  hbim 1009  ax46 1019  ax467 1025  hbimd 1112  sbi2 1235  mo2 1402

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

Copyright terms: Public domain