Theorem ealeh ≪ | index | src | ≫

theorem ealeh {x: nat} (a: nat) (b c: wff x):
  $ F/ x c $ >
  $ x = a -> (b <-> c) $ >
  $ A. x b -> c $;

Step	Hyp	Ref	Expression
1		ax_3	(~c -> ~A. x b) -> A. x b -> c
2		exnal	E. x ~b <-> ~A. x b
3		hyp h	F/ x c
4	3	nfnot	F/ x ~c
5		hyp e	x = a -> (b <-> c)
6	5	noteqd	x = a -> (~b <-> ~c)
7	4, 6	iexeh	~c -> E. x ~b
8	2, 7	sylib	~c -> ~A. x b
9	1, 8	ax_mp	A. 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)