Theorem 19.33-2

Description: Theorem *11.421 in WhiteheadRussell p. 163. Theorem 19.33 of Margaris p. 90 with 2 quantifiers. (Contributed by Andrew Salmon, 24-May-2011)

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

Proof

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