∀x(A(x)→B(x)),∀x(C(x)→┐B(x)) => 推出 ∀x(C(x)

1 ∀x(C(x)→┐B(x))
2 C(y)→┐B(y) 1UI
3 ∀x(A(x)→B(x))
4 A(y)→B(y) 3UI
5 ┐B(y)→┐A(y) 4置换
6 C(y)→┐A(y) 25假言三段论
7 ∀x(C(x)→┐A(x)) 6UG
－－－－－－－－－－
1 ∀xC(x)
2 C(y) 1UI
3 ∀(B(x)→┐C(x)
4 B(y)→┐C(y) 3UI
5 ┐B(y) 24拒取式
6 ∀x(A(x)V B(x))
7 A(y)V B(y) 6UI
8 A(y) 57析取三段论
9 ∀xA(x) 8UG