Theorem _hyp_null_complete ≪ | index | src | ≫

假设为空时补全假设（不可直接引用）

theorem _hyp_null_complete (A G: wff): $ A $ > $ G \imp A $;

Step	Hyp	Ref	Expression
1		introl_imp	A \imp G \imp A
2		hyp h	A
3	1, 2	ax_mp	G \imp A

Axiom use

Logic (ax_mp, ax_1)