FVrC= Vy Sa c Theorem yxc≡ySC, y, provided that y is not free in C and y is free for c in C (1)+mC→SmC AS4 (2)H V.) VySa C 3)h ySCD SSac AS4 (4)F ViSCo VaC (3)>y (5)Fp(p3q)∧(q3p)3(D≡q (6H rC=VySC Logic in Computer Science -p 8/27` ∀xC ≡ ∀ySxyC? Theorem ` ∀xC ≡ ∀ySxy C, provided that y is not free in C and y is free for x in C. (1) ` ∀xC ⊃ Sxy C AS4 (2) ` ∀xC ⊃ ∀ySxy C (1) ⊃ ∀ (3) ` ∀ySxy C ⊃ SyxSxy C AS4 (4) ` ∀ySxy C ⊃ ∀xC (3) ⊃ ∀ (5) |=P (p ⊃ q) ∧ (q ⊃ p) ⊃ (p ≡ q) (6) ` ∀xC ≡ ∀ySxy C Logic in Computer Science – p.8/27