Metamath Proof Explorer


Theorem aaanv

Description: Theorem *11.56 in WhiteheadRussell p. 165. Special case of aaan . (Contributed by Andrew Salmon, 24-May-2011)

Ref Expression
Assertion aaanv ( ( ∀ 𝑥 𝜑 ∧ ∀ 𝑦 𝜓 ) ↔ ∀ 𝑥𝑦 ( 𝜑𝜓 ) )

Proof

Step Hyp Ref Expression
1 nfv 𝑦 𝜑
2 nfv 𝑥 𝜓
3 1 2 aaan ( ∀ 𝑥𝑦 ( 𝜑𝜓 ) ↔ ( ∀ 𝑥 𝜑 ∧ ∀ 𝑦 𝜓 ) )
4 3 bicomi ( ( ∀ 𝑥 𝜑 ∧ ∀ 𝑦 𝜓 ) ↔ ∀ 𝑥𝑦 ( 𝜑𝜓 ) )