トマトが野菜であるなら、トマトサラダは野菜サラダである、の証明

Fx・・・xはトマトである
Gx・・・xは野菜である
Hxy・・・xはyで作られたサラダである
から、トマトサラダは野菜サラダである、は
∀x(∃y(Hxy∧Fy)⊃∃y(Hxy∧Gy))
となる

よって、トマトが野菜であるならトマトサラダは野菜サラダである、は
∀x(Fx⊃Gx)⊃∀x(∃y(Hxy∧Fy)⊃∃y(Hxy∧Gy))
となる。

では、この命題を証明する。
1.∀x(Fx⊃Gx) [1] 前提
2.∃y(Hty∧Fy) [2(t)] 仮定
3.Hta∧Fa [3(a)] 仮定
4.Hta [3(a)] 3を分解
5.Fa [3(a)] 3を分解
6.Fa⊃Ga [1] 1より全称例化
7.Ga[1,3(a)] 5,6より
8.Hta∧Fa⊃Hta∧Ga [1] 3,7より
9.Hta∧Ga [1,2(t)] 2,8より存在例化
10.∃y(Hty∧Gy) [1,2(t)] 9より存在汎化
11.∃y(Hty∧Fy)⊃∃y(Hty∧Gy) [1] 2,9より
12.∀x(∃y(Hxy∧Fy)⊃∃y(Hxy∧Gy) [1] 11より全称汎化
13.∀x(Fx⊃Gx)⊃∀x(∃y(Hxy∧Fy)⊃∃y(Hxy∧Gy) 1,12より証明終了

答えあわせ
9.は8.を経由しなくても、4.と7.から出せる。ただ、そうすると9.の前提が2(t)から3(a)になる。
本と違う証明になったけど、いいのかな？
ということで4.と7.からHta∧Gaを導く場合
8.Hta∧Ga [1,3(a)] 4,7を結合
9.∃y(Hty∧Gy) [1,3(a)] 8を存在汎化
10.(Hta∧Fa)⊃∃y(Hty∧Gy) [1] 3,9から
11.∃y(Hty∧Gy) [1,2(t)] 2,10から存在例化
12.∃y(Hty∧Fy)⊃∃y(Hty∧Gy) 2,11から
13.∀x(∃y(Hxy∧Fy)⊃∃y(Hxy∧Gy) [1] 12より全称汎化
14.∀x(Fx⊃Gx)⊃∀x(∃y(Hxy∧Fy)⊃∃y(Hxy∧Gy) 1,13より証明終了

なんとなく、述語論理の証明法がわかった。
参考にしてる本

論理学