Theorem or_def ≪ | index | src | ≫

\or定义式

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

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

Axiom use

Logic (ax_mp, ax_1, ax_2, ax_3)