Theorem ja 118

Description: Inference joining the antecedents of two premises. (The proof was shortened by Mel L. O'Cat, 30-Aug-04.)

Hypotheses

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

Assertion

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

Proof of Theorem ja

Step	Hyp	Ref	Expression
1		pm2.27 30	. . 3 ⊢ (φ → ((φ → ψ) → ψ))
2		ja.2	. . 3 ⊢ (ψ → χ)
3	1, 2	syl6 23	. 2 ⊢ (φ → ((φ → ψ) → χ))
4		ja.1	. . 3 ⊢ (¬ φ → χ)
5	4	a1d 14	. 2 ⊢ (¬ φ → ((φ → ψ) → χ))
6	3, 5	pm2.61i 110	1 ⊢ ((φ → ψ) → χ)

Syntax hints:  ¬ wn 1   → wi 2

This theorem is referenced by:  hbim 702  hbimd 787  sbi2 885  mo2 1026

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

metamath.org