1 A.x(P(x) -> ~Q(x)) : premise
2 | E.x(P(x) and Q(x)) : assumption
|| with x0
3 || P(x0) and Q(x0) : assumption
4 || P(x0) : and elim1 3
5 || P(x0) -> ~Q(x0) : A.x/x0 elim 1
6 || ~Q(x0) : -> e 5,4
7 || Q(x0) : and elim2 3
8 || contradiction : not elim 6,7
---
9 | contradiction : E.x/x0 elim 2,3-8
---
10 ~(E.x(P(x) and Q(x))) : not introduction 2-9
# Extraneous step #s in the src are ignored. Be careful.
1 A.x(P(x,z))
| with y0
2 | P(y0,z) : A.x/y0 e 1
---
3 A.y(P(y,z)) : A.y/y0 i 2-2
# Sloppy syntax is fine :-)
P(a)
| with x0
|| a = x0 : assumption
|| P(x0) : = e 2,1
-
| a = x0 -> P(x0) : -> i 2-3
-
A.x(a=x->P(x)) : A.x/x0 i 2-4
1 A.x(Q(x) -> R(x)) : premise
2 E.x(P(x) and Q(x)) : premise
| with x0
3 | P(x0) and Q(x0) : assumption
4 | Q(x0) -> R(x0) : A.x/x0 e 1
5 | Q(x0) : and e2 3
6 | R(x0) : -> e 4,5
7 | P(x0) : and e1 3
8 | P(x0) and R(x0) : and i 7,6
9 | E.x(P(x) and R(x)) : E.x/x0 i 8
---
10 E.x(P(x) and R(x)) : E.x/x0 e 2, 3-9