Due to symbol constraints, the following substitutions have been made to the normal symbolization: conjunction is symbolized with an ampersand (&) rather than the dot; conditional is symbolized with a dash and angle bracket (->) rather than the horseshoe; biconditional is symbolized with an angle bracket, dash, and angle bracket (<->) rather than the triple-bar; the existential quantifier is a capital "E", rather than a backwards "E".

The conclusion immediately follows the last premise, and is enclosed in square brackets [ ].

1. (x)Fx [ /.: (Ex)Fx ]

1. (Ex)Fx

2. (x)(Fx -> ~Gx) [ /.: (Ex)~Gx ]

1. (x)~(Gx & Hx)

2. (Ex)(Fx & Gx) [ /.: (Ex)(Fx & ~Hx) ]

1. (x)(Hx -> Gx)

2. (Ex)(~Gx & Fx) [ /.: (Ex)(Fx & ~Hx) ]

1. (x)(Gx -> Hx)

2. (Ex)(Gx & Fx) [ /.: (Ex)(Fx & Hx) ]

1. (Ex)(Gx & Hx)

2. (x)(Gx -> Fx) [ /.: (Ex)(Fx & Hx) ]

1. (Ex)(~Fx & ~Gx)

2. (x)(~Gx -> ~Hx) [ /.: (Ex)(~Hx & ~Fx) ]

1. (x)(Fx -> (Gx -> ~Hx))

2. (Ey)(Hy & Fy) [ /.: (Ex)~Gx ]

1. (x)(Fx v ~Gx)

2. (x)(Fx -> Hx)

3. (x)(~Gx -> Jx)

4. (Ex)~Jx [ /.: (Ex)Hx ]

1. (x)(Fx <-> Gx)

2. (x)(Gx -> Hx)

3. (Ex)(Fx v Gx) [ /.: (Ex)(Fx & Hx) ]

1. (x)(Fx & Gx) [ /.: (x)Fx & (x)Gx ]

1. (x)Fx & (x)Gx [ /.: (x)(Fx &Gx) ]

1. (x)(Fx <-> Gx)

2. (x)Fx [ /.: (x)Gx ]

1. (x)(Fx <-> (Gx & Hx) [ /.: (x)(Fx -> Gx) & (x)(Fx -> Hx) ]

1. (x)((Fx v Gx) -> Hx) [ /.: (x)(Fx -> Hx) & (x)(Gx -> Hx) ]

1. (z)(Fz -> Hz)

2. (z)(Gz -> Hz) [ /.: (z)((Fz v Gz) -> Hz) ]

1. (x)(Fx <-> (~Gx & ~Fx)) [ /.: (x)Gx ]

1. (y)(Fy <-> (~Gy -> ~Fy)) [ /.: (y)Gy ]

1. (x)((Fx & Gx) -> Hx)

2. (x)Gx & (x)(Fx) [ /.: (y)(Fy & Hy) ]

1. (x)(Fx -> (Gx v Hx))

2. (x)((Jx & Fx) -> ~Gx)

3. (x)(~Fx -> ~Jx) [ /.: (x)(Jx -> Hx)]

[ /.: ( (x)Fx & (x)Gx ) <-> (x)(Fx &Gx) ]

(This is a tautology, and hence must be proven with no premises.)