Theorem ealdeh ≪ | index | src | ≫ 

theorem ealdeh {x: nat} (a: nat) (G b c: wff x):
  $ F/ x G $ >
  $ F/ x c $ >
  $ G /\ x = a -> b -> c $ >
  $ G -> A. x b -> c $;
StepHypRefExpression
1 exnal 
E. x ~b <-> ~A. x b
2 hyp h1 
F/ x G
3 hyp h2 
F/ x c
4 3 nfnot 
F/ x ~c
5 2, 4 nfan 
F/ x G /\ ~c
6 hyp e 
G /\ x = a -> b -> c
7 6 con3d 
G /\ x = a -> ~c -> ~b
8 7 imp 
G /\ x = a /\ ~c -> ~b
9 8 anrasss 
G /\ ~c /\ x = a -> ~b
10 5, 9 iexdeh 
G /\ ~c -> E. x ~b
11 1, 10 sylib 
G /\ ~c -> ~A. x b
12 11 exp 
G -> ~c -> ~A. x b
13 12 con4d 
G -> 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)