Dependent Axioms

P(i(i(i(x,y),x),x)) % A3

• A3 not in shorter proofs of T1 and (T2 & T3)
• A3 removed from axioms
• A3 found in a proof of T1
• A3 later proved without A6 or A7

P(i(j(x,j(y,z)),j(y,j(x,z)))) % A6

• T1 proved without A6
• A6 proved without A3 or A7

P(i(j(j(x,y),x),x)) % A7

• Not dependent, but more about that later