Theorem jaodd

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

	Ref	Expression
Hypotheses	jaodd.1	⊢ ( 𝜑 → ( 𝜓 → ( 𝜒 → 𝜃 ) ) )
	jaodd.2	⊢ ( 𝜑 → ( 𝜓 → ( 𝜏 → 𝜃 ) ) )
Assertion	jaodd	⊢ ( 𝜑 → ( 𝜓 → ( ( 𝜒 ∨ 𝜏 ) → 𝜃 ) ) )

Proof

Step	Hyp	Ref	Expression
1		jaodd.1	⊢ ( 𝜑 → ( 𝜓 → ( 𝜒 → 𝜃 ) ) )
2		jaodd.2	⊢ ( 𝜑 → ( 𝜓 → ( 𝜏 → 𝜃 ) ) )
3		jao	⊢ ( ( 𝜒 → 𝜃 ) → ( ( 𝜏 → 𝜃 ) → ( ( 𝜒 ∨ 𝜏 ) → 𝜃 ) ) )
4	1 2 3	syl6c	⊢ ( 𝜑 → ( 𝜓 → ( ( 𝜒 ∨ 𝜏 ) → 𝜃 ) ) )