Theorem alimd ≪ | index | src | ≫

theorem alimd {x: nat} (G: wff) (a b: wff x):
  $ G -> a -> b $ >
  $ G -> A. x a -> A. x b $;

Step	Hyp	Ref	Expression
1		ax_4	A. x (a -> b) -> A. x a -> A. x b
2		hyp h	G -> a -> b
3	2	alimi	A. x G -> A. x (a -> b)
4		ax_5	G -> A. x G
5	3, 4	syl	G -> A. x (a -> b)
6	1, 5	syl	G -> A. x a -> A. x b

Axiom use

axs_prop_calc (ax_1, ax_2, ax_mp), axs_pred_calc (ax_gen, ax_4, ax_5)