Theorem aaan

Description: Distribute universal quantifiers. (Contributed by NM, 12-Aug-1993) Avoid ax-10 . (Revised by Gino Giotto, 21-Nov-2024)

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

Proof

Step	Hyp	Ref	Expression
1		aaan.1	⊢ Ⅎ 𝑦 𝜑
2		aaan.2	⊢ Ⅎ 𝑥 𝜓
3		19.26-2	⊢ ( ∀ 𝑥 ∀ 𝑦 ( 𝜑 ∧ 𝜓 ) ↔ ( ∀ 𝑥 ∀ 𝑦 𝜑 ∧ ∀ 𝑥 ∀ 𝑦 𝜓 ) )
4	1	19.3	⊢ ( ∀ 𝑦 𝜑 ↔ 𝜑 )
5	4	albii	⊢ ( ∀ 𝑥 ∀ 𝑦 𝜑 ↔ ∀ 𝑥 𝜑 )
6		alcom	⊢ ( ∀ 𝑥 ∀ 𝑦 𝜓 ↔ ∀ 𝑦 ∀ 𝑥 𝜓 )
7	2	19.3	⊢ ( ∀ 𝑥 𝜓 ↔ 𝜓 )
8	7	albii	⊢ ( ∀ 𝑦 ∀ 𝑥 𝜓 ↔ ∀ 𝑦 𝜓 )
9	6 8	bitri	⊢ ( ∀ 𝑥 ∀ 𝑦 𝜓 ↔ ∀ 𝑦 𝜓 )
10	5 9	anbi12i	⊢ ( ( ∀ 𝑥 ∀ 𝑦 𝜑 ∧ ∀ 𝑥 ∀ 𝑦 𝜓 ) ↔ ( ∀ 𝑥 𝜑 ∧ ∀ 𝑦 𝜓 ) )
11	3 10	bitri	⊢ ( ∀ 𝑥 ∀ 𝑦 ( 𝜑 ∧ 𝜓 ) ↔ ( ∀ 𝑥 𝜑 ∧ ∀ 𝑦 𝜓 ) )