Theorem _hyp_collect ≪ | index | src | ≫

假设不为空时对移出的假设进行收集（不可直接引用）

theorem _hyp_collect (A G_1 G_2 G_3: wff):
  $ G_1 \imp G_2 \imp G_3 \imp A $ >
  $ G_1 \imp G_2 \and G_3 \imp A $;
StepHypRefExpression
1 imp_tran 
(G_1 \imp G_2 \imp G_3 \imp A) \imp ((G_2 \imp G_3 \imp A) \imp G_2 \and G_3 \imp A) \imp G_1 \imp G_2 \and G_3 \imp A
2 hyp h 
G_1 \imp G_2 \imp G_3 \imp A
3 1, 2 ax_mp 
((G_2 \imp G_3 \imp A) \imp G_2 \and G_3 \imp A) \imp G_1 \imp G_2 \and G_3 \imp A
4 imp_nested_assemb_and 
(G_2 \imp G_3 \imp A) \imp G_2 \and G_3 \imp A
5 3, 4 ax_mp 
G_1 \imp G_2 \and G_3 \imp A

Axiom use

Logic (ax_mp, ax_1, ax_2, ax_3)