Theorem nfnlem2 ≪ | index | src | ≫

theorem nfnlem2 {x y z: nat} (c: nat y z) (a b d: nat x):
  $ y = a /\ z = b -> c = d $ >
  $ FN/ x a $ >
  $ FN/ x b $ >
  $ FN/ x d $;

Step	Hyp	Ref	Expression
1		eqcom	N[a / y] N[b / z] c = d -> d = N[a / y] N[b / z] c
2		hyp e	y = a /\ z = b -> c = d
3	2	sbned	y = a -> N[b / z] c = d
4	3	sbne	N[a / y] N[b / z] c = d
5	1, 4	ax_mp	d = N[a / y] N[b / z] c
6		hyp h1	FN/ x a
7		hyp h2	FN/ x b
8		nfnv	FN/ x c
9	7, 8	nfsbnh	FN/ x N[b / z] c
10	6, 9	nfsbnh	FN/ x N[a / y] N[b / z] c
11	5, 10	nfnx	FN/ x d

Axiom use

axs_prop_calc (ax_1, ax_2, ax_3, ax_mp, itru), axs_pred_calc (ax_gen, ax_4, ax_5, ax_6, ax_7, ax_10, ax_11, ax_12), axs_set (elab, ax_8), axs_the (theid, the0)