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	|- (-. ph -> ch)
ja.2	|- (ps -> ch)

Assertion

Ref	Expression
ja	|- ((ph -> ps) -> ch)

Proof of Theorem ja

Step	Hyp	Ref	Expression
1		pm2.27 30	. . 3 |- (ph -> ((ph -> ps) -> ps))
2		ja.2	. . 3 |- (ps -> ch)
3	1, 2	syl6 23	. 2 |- (ph -> ((ph -> ps) -> ch))
4		ja.1	. . 3 |- (-. ph -> ch)
5	4	a1d 14	. 2 |- (-. ph -> ((ph -> ps) -> ch))
6	3, 5	pm2.61i 110	1 |- ((ph -> ps) -> ch)

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