theorem nfim {x: nat} (a b: wff x): $ F/ x a $ > $ F/ x b $ > $ F/ x a -> b $;
Step | Hyp | Ref | Expression |
1 |
|
ax_1 |
b -> a -> b |
2 |
1 |
alimi |
A. x b -> A. x (a -> b) |
3 |
|
hyp h2 |
F/ x b |
4 |
3 |
nfi |
b -> A. x b |
5 |
2, 4 |
syl |
b -> A. x (a -> b) |
6 |
|
mpcom |
a -> (a -> b) -> b |
7 |
5, 6 |
syl6 |
a -> (a -> b) -> A. x (a -> b) |
8 |
|
absurd |
~a -> a -> b |
9 |
8 |
alimi |
A. x ~a -> A. x (a -> b) |
10 |
|
hyp h1 |
F/ x a |
11 |
10 |
nfnot |
F/ x ~a |
12 |
11 |
nfi |
~a -> A. x ~a |
13 |
9, 12 |
syl |
~a -> A. x (a -> b) |
14 |
13 |
a1d |
~a -> (a -> b) -> A. x (a -> b) |
15 |
7, 14 |
cases |
(a -> b) -> A. x (a -> b) |
16 |
15 |
nfri |
F/ x a -> b |
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)