Theorem 19.21-2

Description: Version of 19.21 with two quantifiers. (Contributed by NM, 4-Feb-2005)

	Ref	Expression
Hypotheses	19.21-2.1	⊢ Ⅎ 𝑥 𝜑
	19.21-2.2	⊢ Ⅎ 𝑦 𝜑
Assertion	19.21-2	⊢ ( ∀ 𝑥 ∀ 𝑦 ( 𝜑 → 𝜓 ) ↔ ( 𝜑 → ∀ 𝑥 ∀ 𝑦 𝜓 ) )

Proof

Step	Hyp	Ref	Expression
1		19.21-2.1	⊢ Ⅎ 𝑥 𝜑
2		19.21-2.2	⊢ Ⅎ 𝑦 𝜑
3	2	19.21	⊢ ( ∀ 𝑦 ( 𝜑 → 𝜓 ) ↔ ( 𝜑 → ∀ 𝑦 𝜓 ) )
4	3	albii	⊢ ( ∀ 𝑥 ∀ 𝑦 ( 𝜑 → 𝜓 ) ↔ ∀ 𝑥 ( 𝜑 → ∀ 𝑦 𝜓 ) )
5	1	19.21	⊢ ( ∀ 𝑥 ( 𝜑 → ∀ 𝑦 𝜓 ) ↔ ( 𝜑 → ∀ 𝑥 ∀ 𝑦 𝜓 ) )
6	4 5	bitri	⊢ ( ∀ 𝑥 ∀ 𝑦 ( 𝜑 → 𝜓 ) ↔ ( 𝜑 → ∀ 𝑥 ∀ 𝑦 𝜓 ) )