Theorem alimi | index | src |

theorem alimi {x: nat} (a b: wff x): $ a -> b $ > $ A. x a -> A. x b $;
StepHypRefExpression
1 ax_4
A. x (a -> b) -> A. x a -> A. x b
2 hyp h
a -> b
3 2 ax_gen
A. x (a -> b)
4 1, 3 ax_mp
A. x a -> A. x b

Axiom use

axs_prop_calc (ax_mp), axs_pred_calc (ax_gen, ax_4)