Theorem _hyp_null_intro ≪ | index | src | ≫

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

theorem _hyp_null_intro (G: wff): $ G \imp G $;

Step	Hyp	Ref	Expression
1		imp_refl	G \imp G

Axiom use

Logic (ax_mp, ax_1, ax_2)