Description: Theorem *10.252 in WhiteheadRussell p. 149. (Contributed by Andrew Salmon, 17-Jun-2011) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Assertion | pm10.252 | |- ( -. E. x ph <-> A. x -. ph ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-ex | |- ( E. x ph <-> -. A. x -. ph ) |
|
2 | 1 | bicomi | |- ( -. A. x -. ph <-> E. x ph ) |
3 | 2 | con1bii | |- ( -. E. x ph <-> A. x -. ph ) |