Theorem indd ≪ | index | src | ≫ 

theorem indd (G: wff) {x y: nat} (a: nat y) (px: wff x) (p0 pa py ps: wff y):
  $ x = a -> (px <-> pa) $ >
  $ x = 0 -> (px <-> p0) $ >
  $ x = y -> (px <-> py) $ >
  $ x = suc y -> (px <-> ps) $ >
  $ G -> p0 $ >
  $ G /\ py -> ps $ >
  $ G -> pa $;
StepHypRefExpression
1 hyp ha 
x = a -> (px <-> pa)
2 1 imeq2d 
x = a -> (G -> px <-> G -> pa)
3 hyp h0 
x = 0 -> (px <-> p0)
4 3 imeq2d 
x = 0 -> (G -> px <-> G -> p0)
5 hyp hy 
x = y -> (px <-> py)
6 5 imeq2d 
x = y -> (G -> px <-> G -> py)
7 hyp hs 
x = suc y -> (px <-> ps)
8 7 imeq2d 
x = suc y -> (G -> px <-> G -> ps)
9 hyp h1 
G -> p0
10 hyp h2 
G /\ py -> ps
11 10 exp 
G -> py -> ps
12 11 a2i 
(G -> py) -> G -> ps
13 2, 4, 6, 8, 9, 12 ind 
G -> pa

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_peano (peano2, peano5)