Metamath Proof Explorer

Theorem pm10.251

Description: Theorem *10.251 in WhiteheadRussell p. 149. (Contributed by Andrew Salmon, 17-Jun-2011)

Ref Expression
Assertion pm10.251 
|- ( A. x -. ph -> -. A. x ph )

Proof

Step Hyp Ref Expression
1 alnex 
 |-  ( A. x -. ph <-> -. E. x ph )
2 19.2 
 |-  ( A. x ph -> E. x ph )
3 2 con3i 
 |-  ( -. E. x ph -> -. A. x ph )
4 1 3 sylbi 
 |-  ( A. x -. ph -> -. A. x ph )