Theorem or_elimr ≪ | index | src | ≫

\or右消除

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

Step	Hyp	Ref	Expression
1		neg_imp_swap	(\neg A \imp B) \imp \neg B \imp A
2	1	conv or	A \or B \imp \neg B \imp A

Axiom use

Logic (ax_mp, ax_1, ax_2, ax_3)