Theorem 19.33

Description: Theorem 19.33 of Margaris p. 90. (Contributed by NM, 12-Mar-1993)

	Ref	Expression
Assertion	19.33	⊢ ( ( ∀ 𝑥 𝜑 ∨ ∀ 𝑥 𝜓 ) → ∀ 𝑥 ( 𝜑 ∨ 𝜓 ) )

Proof

Step	Hyp	Ref	Expression
1		orc	⊢ ( 𝜑 → ( 𝜑 ∨ 𝜓 ) )
2	1	alimi	⊢ ( ∀ 𝑥 𝜑 → ∀ 𝑥 ( 𝜑 ∨ 𝜓 ) )
3		olc	⊢ ( 𝜓 → ( 𝜑 ∨ 𝜓 ) )
4	3	alimi	⊢ ( ∀ 𝑥 𝜓 → ∀ 𝑥 ( 𝜑 ∨ 𝜓 ) )
5	2 4	jaoi	⊢ ( ( ∀ 𝑥 𝜑 ∨ ∀ 𝑥 𝜓 ) → ∀ 𝑥 ( 𝜑 ∨ 𝜓 ) )