Theorem introl_imp ≪ | index | src | ≫

左引入\imp

theorem introl_imp (A B: wff): $ A \imp B \imp A $;

Step	Hyp	Ref	Expression
1		ax_1	A \imp B \imp A

Axiom use

Logic (ax_1)