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 
|- ( ( A. x ph /\ A. y ps ) <-> A. x A. y ( ph /\ ps ) )

Proof

Step Hyp Ref Expression
1 nfv 
 |-  F/ y ph
2 nfv 
 |-  F/ x ps
3 1 2 aaan 
 |-  ( A. x A. y ( ph /\ ps ) <-> ( A. x ph /\ A. y ps ) )
4 3 bicomi 
 |-  ( ( A. x ph /\ A. y ps ) <-> A. x A. y ( ph /\ ps ) )