Theorem intror_or ≪ | index | src | ≫

\or右引入

theorem intror_or (A B: wff): $ A \imp A \or B $;
StepHypRefExpression
1 intror_neg_imp 
A \imp \neg A \imp B
2 1 conv or 
A \imp A \or B

Axiom use

Logic (ax_mp, ax_1, ax_2, ax_3)