Theorem eexdh ≪ | index | src | ≫

theorem eexdh {x: nat} (a b c: wff x):
  $ F/ x a $ >
  $ F/ x c $ >
  $ a -> b -> c $ >
  $ a -> E. x b -> c $;

Step	Hyp	Ref	Expression
1		hyp h1	F/ x a
2		hyp h2	F/ x c
3	2	nfnot	F/ x ~c
4	1, 3	nfan	F/ x a /\ ~c
5		hyp h3	a -> b -> c
6	5	con3d	a -> ~c -> ~b
7	6	imp	a /\ ~c -> ~b
8	4, 7	ialdh	a /\ ~c -> A. x ~b
9	8	exp	a -> ~c -> A. x ~b
10	9	con1d	a -> ~A. x ~b -> c
11	10	conv ex	a -> E. x b -> 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_10, ax_12)