Theorem aaan

Description: Rearrange universal quantifiers. (Contributed by NM, 12-Aug-1993)

	Ref	Expression
Hypotheses	aaan.1	⊢ Ⅎ 𝑦 𝜑
	aaan.2	⊢ Ⅎ 𝑥 𝜓
Assertion	aaan	⊢ ( ∀ 𝑥 ∀ 𝑦 ( 𝜑 ∧ 𝜓 ) ↔ ( ∀ 𝑥 𝜑 ∧ ∀ 𝑦 𝜓 ) )

Proof

Step	Hyp	Ref	Expression
1		aaan.1	⊢ Ⅎ 𝑦 𝜑
2		aaan.2	⊢ Ⅎ 𝑥 𝜓
3	1	19.28	⊢ ( ∀ 𝑦 ( 𝜑 ∧ 𝜓 ) ↔ ( 𝜑 ∧ ∀ 𝑦 𝜓 ) )
4	3	albii	⊢ ( ∀ 𝑥 ∀ 𝑦 ( 𝜑 ∧ 𝜓 ) ↔ ∀ 𝑥 ( 𝜑 ∧ ∀ 𝑦 𝜓 ) )
5	2	nfal	⊢ Ⅎ 𝑥 ∀ 𝑦 𝜓
6	5	19.27	⊢ ( ∀ 𝑥 ( 𝜑 ∧ ∀ 𝑦 𝜓 ) ↔ ( ∀ 𝑥 𝜑 ∧ ∀ 𝑦 𝜓 ) )
7	4 6	bitri	⊢ ( ∀ 𝑥 ∀ 𝑦 ( 𝜑 ∧ 𝜓 ) ↔ ( ∀ 𝑥 𝜑 ∧ ∀ 𝑦 𝜓 ) )