Theorem jad

Description: Deduction form of ja . (Contributed by Scott Fenton, 13-Dec-2010) (Proof shortened by Andrew Salmon, 17-Sep-2011)

	Ref	Expression
Hypotheses	jad.1	|- ( ph -> ( -. ps -> th ) )
	jad.2	|- ( ph -> ( ch -> th ) )
Assertion	jad	|- ( ph -> ( ( ps -> ch ) -> th ) )

Proof

Step	Hyp	Ref	Expression
1		jad.1	|- ( ph -> ( -. ps -> th ) )
2		jad.2	|- ( ph -> ( ch -> th ) )
3	1	com12	|- ( -. ps -> ( ph -> th ) )
4	2	com12	|- ( ch -> ( ph -> th ) )
5	3 4	ja	|- ( ( ps -> ch ) -> ( ph -> th ) )
6	5	com12	|- ( ph -> ( ( ps -> ch ) -> th ) )