Description: Theorem *10.12 in WhiteheadRussell p. 146. In *10, this is treated as an axiom, and the proofs in *10 are based on this theorem. (Contributed by Andrew Salmon, 17-Jun-2011)
Ref | Expression | ||
---|---|---|---|
Assertion | pm10.12 | |- ( A. x ( ph \/ ps ) -> ( ph \/ A. x ps ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 19.32v | |- ( A. x ( ph \/ ps ) <-> ( ph \/ A. x ps ) ) |
|
2 | 1 | biimpi | |- ( A. x ( ph \/ ps ) -> ( ph \/ A. x ps ) ) |