Description: Theorem *11.56 in WhiteheadRussell p. 165. Special case of aaan . (Contributed by Andrew Salmon, 24-May-2011)
Ref | Expression | ||
---|---|---|---|
Assertion | aaanv | ⊢ ( ( ∀ 𝑥 𝜑 ∧ ∀ 𝑦 𝜓 ) ↔ ∀ 𝑥 ∀ 𝑦 ( 𝜑 ∧ 𝜓 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfv | ⊢ Ⅎ 𝑦 𝜑 | |
2 | nfv | ⊢ Ⅎ 𝑥 𝜓 | |
3 | 1 2 | aaan | ⊢ ( ∀ 𝑥 ∀ 𝑦 ( 𝜑 ∧ 𝜓 ) ↔ ( ∀ 𝑥 𝜑 ∧ ∀ 𝑦 𝜓 ) ) |
4 | 3 | bicomi | ⊢ ( ( ∀ 𝑥 𝜑 ∧ ∀ 𝑦 𝜓 ) ↔ ∀ 𝑥 ∀ 𝑦 ( 𝜑 ∧ 𝜓 ) ) |