Theorem _hyp_null_collect ≪ | index | src | ≫

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

theorem _hyp_null_collect (A G_1 G_2: wff):
  $ G_1 \imp G_2 \imp A $ >
  $ G_1 \and G_2 \imp A $;

Step	Hyp	Ref	Expression
1		imp_nested_assemb_and	(G_1 \imp G_2 \imp A) \imp G_1 \and G_2 \imp A
2		hyp h	G_1 \imp G_2 \imp A
3	1, 2	ax_mp	G_1 \and G_2 \imp A

Axiom use

Logic (ax_mp, ax_1, ax_2, ax_3)