这里我们看一个比较复杂的例子。
　例5
　　有的病人喜欢所有的医生, 没有一个病人喜欢某一庸医,所以没有医生是庸医。
　　先形式化。令
　　P(x)表x是病人，Q(x)表x是庸医。
　　D(x)表x是医生，L(x, y)表x喜欢y。
　　第一句话可描述为
　　(x)(P(x)∧(y)(D(y)→L(x, y)))
　　第二句话可描述为
　　(x)(P(x)→(y)(Q(y)→L(x, y)))
　　或写成
　　(x)(P(x)∧(y)(Q(y)∧L(x, y)))
　　结论可描述为
　　(x)(D(x)→Q(x))
　　或写成
　　(x)(D(x)∧Q(x))
　　证明
　　(1) (x)(P(x)∧(y)(D(y)→L(x, y))) 前提
　　(2) P(c)∧(y)(D(y)→L(c, y)) (1)存在量词消去
　　(3) (x)(P(x)→(y)(Q(y)→L(x, y))) 前提
　　(4) P(c)→(y)(Q(y)→L(c, y)) (3)全称量词消去
　　(5) P(c) (2)
　　(6) (y)(D(y)→L(c, y)) (2)
　　(7) D(y)→L(c, y) (6)全称量词消去
　　(8) (y)(Q(y)→L(c, y)) (4)(5)分离
　　(9) Q(y)→L(c, y) (8)全称量词消去
　　(10) L(c, y)→Q(y) (9)置换
　　(11) D(y)→Q(y) (7)(10)假言三段论
　　(12) (y)(D(y)→Q(y)) (11)全称量词引入
　　(13) (x)(D(x)→Q(x)) (12)置换
　在形式证明中，如果有的前提不带量词，但又需要将其中的某个自由变元换成一个特定的个体，这实际上是个代入的问题。由于形式证明时要根据推理规则逐步进行，所以不能直接代入，可先用UG一般化（即加上全称量词）然后再用US特定化（即去掉全称量词而将变元换成另一变元或某个个体），再用UG或EG一般化（即加上量词并把变元或个体换成要改名的变元）。当然，在运用这些规则时都要注意规则的条件。具体步骤如下：
　　将P(x)中的自由变元代入以变元y：
　　（1）P(x) 前提
　　（2）x P(x) （1）UG
　　（3）P(y) （2）US
　　将P(x)中的自由变元代入以个体a：  
　　（1）P(x) 前提
　　（2）x P(x) （1）UG
　　（3）P(a) （2）US
　　将$x P(x)中的x改名为y：  
　　（1）x P(x) 前提
　　（2）P(a) （1）ES
　　（3）x P(y) （2）EG
　　将x P(x)中的x改名为y：  
　　（1）x P(x) 前提
　　（2）P(x) （1）US
　　（3）y P(y) （2）UG