The Logic Book, M. Bergmann, J. Moor, J. Nelson, McGraw Hill, 2004, 10.5E, 3(d), p. 563

Is the following a theorem of predicate logic: (x)(Ax ⊃Bx) ∨(∃x)Ax ? Yes, it is provable without premises, and the proof is straightforward.

1. (x)(Ax ⊃Bx) ∨(∃x)Ax
2. * ¬ (x)(Ax ⊃Bx) ......... ACP
3. * (∃x)(Ax • ¬ Bx) ......... 2CQ
4. * An • ¬ Bn ......... 3EI x/n
5. * An ......... 4Simpl.
6. * (∃x)Ax ......... 5EG
7. ¬ (x)(Ax ⊃Bx) ⊃(∃x)Ax ......... 2-6CP
8. ¬ ¬ (x)(Ax ⊃Bx) ∨(∃x)Ax ......... 7MI
9. (x)(Ax ⊃Bx) ∨(∃x)Ax ......... 8DN