∀x(A(x)→B(x)),∀x(C(x)→┐B(x)) => 推出 ∀x(C(x)→┐A(x))∀x(A(x)V B(x)),∀(B(x)→┐C(x),∀C(x) ,∀xC(x) => 推出 ∀xA(x)证明以上两个式子.

∀x(A(x)→B(x)),∀x(C(x)→┐B(x)) => 推出 ∀x(C(x)→┐A(x))∀x(A(x)V B(x)),∀(B(x)→┐C(x),∀C(x) ,∀xC(x) => 推出 ∀xA(x)证明以上两个式子.
∀x(A(x)→B(x)),∀x(C(x)→┐B(x)) => 推出 ∀x(C(x)→┐A(x))
∀x(A(x)V B(x)),∀(B(x)→┐C(x),∀C(x) ,∀xC(x) => 推出 ∀xA(x)
证明以上两个式子.

∀x(A(x)→B(x)),∀x(C(x)→┐B(x)) => 推出 ∀x(C(x)→┐A(x))∀x(A(x)V B(x)),∀(B(x)→┐C(x),∀C(x) ,∀xC(x) => 推出 ∀xA(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