Theorem iexdde ≪ | index | src | ≫

theorem iexdde {x: nat} (G b: wff) (a: nat) (c: wff x):
  $ G /\ x = a -> b -> c $ >
  $ G -> b -> E. x c $;

Step	Hyp	Ref	Expression
1		hyp e	G /\ x = a -> b -> c
2	1	exp	G -> x = a -> b -> c
3	2	com23	G -> b -> x = a -> c
4	3	imp	G /\ b -> x = a -> c
5	4	imp	G /\ b /\ x = a -> c
6	5	iexde	G /\ b -> E. x c
7	6	exp	G -> b -> E. x c

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_12)