Theorem _hyp_intro ≪ | index | src | ≫

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

theorem _hyp_intro (A G: wff): $ G \and A \imp A $;

Step	Hyp	Ref	Expression
1		and_splitr	G \and A \imp A

Axiom use

Logic (ax_mp, ax_1, ax_2, ax_3)