Theorem jaodd

Description: Double deduction form of jaoi . (Contributed by Steven Nguyen, 17-Jul-2022)

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

Proof

Step	Hyp	Ref	Expression
1		jaodd.1	|- ( ph -> ( ps -> ( ch -> th ) ) )
2		jaodd.2	|- ( ph -> ( ps -> ( ta -> th ) ) )
3		jao	|- ( ( ch -> th ) -> ( ( ta -> th ) -> ( ( ch \/ ta ) -> th ) ) )
4	1 2 3	syl6c	|- ( ph -> ( ps -> ( ( ch \/ ta ) -> th ) ) )