Theorem imp_left_intro ≪ | index | src | ≫

→左引入

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

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

Axiom use

ZFC (ax_p1)