Metamath Proof Explorer

Theorem 2exanali

Description: Theorem *11.521 in WhiteheadRussell p. 164. (Contributed by Andrew Salmon, 24-May-2011)

Ref Expression
Assertion 2exanali 
|- ( -. E. x E. y ( ph /\ -. ps ) <-> A. x A. y ( ph -> ps ) )

Proof

Step Hyp Ref Expression
1 2nalexn 
 |-  ( -. A. x A. y ( ph -> ps ) <-> E. x E. y -. ( ph -> ps ) )
2 1 con1bii 
 |-  ( -. E. x E. y -. ( ph -> ps ) <-> A. x A. y ( ph -> ps ) )
3 annim 
 |-  ( ( ph /\ -. ps ) <-> -. ( ph -> ps ) )
4 3 2exbii 
 |-  ( E. x E. y ( ph /\ -. ps ) <-> E. x E. y -. ( ph -> ps ) )
5 2 4 xchnxbir 
 |-  ( -. E. x E. y ( ph /\ -. ps ) <-> A. x A. y ( ph -> ps ) )