Theorem 3jaodd

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

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

Proof

Step	Hyp	Ref	Expression
1		3jaodd.1	⊢ ( 𝜑 → ( 𝜓 → ( 𝜒 → 𝜂 ) ) )
2		3jaodd.2	⊢ ( 𝜑 → ( 𝜓 → ( 𝜃 → 𝜂 ) ) )
3		3jaodd.3	⊢ ( 𝜑 → ( 𝜓 → ( 𝜏 → 𝜂 ) ) )
4	1	com3r	⊢ ( 𝜒 → ( 𝜑 → ( 𝜓 → 𝜂 ) ) )
5	2	com3r	⊢ ( 𝜃 → ( 𝜑 → ( 𝜓 → 𝜂 ) ) )
6	3	com3r	⊢ ( 𝜏 → ( 𝜑 → ( 𝜓 → 𝜂 ) ) )
7	4 5 6	3jaoi	⊢ ( ( 𝜒 ∨ 𝜃 ∨ 𝜏 ) → ( 𝜑 → ( 𝜓 → 𝜂 ) ) )
8	7	com3l	⊢ ( 𝜑 → ( 𝜓 → ( ( 𝜒 ∨ 𝜃 ∨ 𝜏 ) → 𝜂 ) ) )