Theorem nfnot | index | src |

theorem nfnot {x: nat} (a: wff x): $ F/ x a $ > $ F/ x ~a $;
StepHypRefExpression
1 con1
(~A. x ~a -> a) -> ~a -> A. x ~a
2 eal
A. x a -> a
3 con1
(~A. x a -> A. x ~A. x a) -> ~A. x ~A. x a -> A. x a
4 ax_10
~A. x a -> A. x ~A. x a
5 3, 4 ax_mp
~A. x ~A. x a -> A. x a
6 hyp h
F/ x a
7 6 nfi
a -> A. x a
8 7 eximi
E. x a -> E. x A. x a
9 8 conv ex
~A. x ~a -> ~A. x ~A. x a
10 5, 9 syl
~A. x ~a -> A. x a
11 2, 10 syl
~A. x ~a -> a
12 1, 11 ax_mp
~a -> A. x ~a
13 12 nfri
F/ x ~a

Axiom use

axs_prop_calc (ax_1, ax_2, ax_3, ax_mp), axs_pred_calc (ax_gen, ax_4, ax_5, ax_6, ax_7, ax_10, ax_12)