Theorem 3jaodd

Description: Double deduction form of 3jaoi . (Contributed by Scott Fenton, 20-Apr-2011)

	Ref	Expression
Hypotheses	3jaodd.1	|- ( ph -> ( ps -> ( ch -> et ) ) )
	3jaodd.2	|- ( ph -> ( ps -> ( th -> et ) ) )
	3jaodd.3	|- ( ph -> ( ps -> ( ta -> et ) ) )
Assertion	3jaodd	|- ( ph -> ( ps -> ( ( ch \/ th \/ ta ) -> et ) ) )

Proof

Step	Hyp	Ref	Expression
1		3jaodd.1	|- ( ph -> ( ps -> ( ch -> et ) ) )
2		3jaodd.2	|- ( ph -> ( ps -> ( th -> et ) ) )
3		3jaodd.3	|- ( ph -> ( ps -> ( ta -> et ) ) )
4	1	com3r	|- ( ch -> ( ph -> ( ps -> et ) ) )
5	2	com3r	|- ( th -> ( ph -> ( ps -> et ) ) )
6	3	com3r	|- ( ta -> ( ph -> ( ps -> et ) ) )
7	4 5 6	3jaoi	|- ( ( ch \/ th \/ ta ) -> ( ph -> ( ps -> et ) ) )
8	7	com3l	|- ( ph -> ( ps -> ( ( ch \/ th \/ ta ) -> et ) ) )