Theorem introl_or ≪ | index | src | ≫

\or左引入

theorem introl_or (A B: wff): $ B \imp A \or B $;

Step	Hyp	Ref	Expression
1		introl_imp	B \imp \neg A \imp B
2	1	conv or	B \imp A \or B

Axiom use

Logic (ax_1)