Theorem or_unify ≪ | index | src | ≫

\or归一

theorem or_unify (A: wff): $ A \or A \iff A $;


((\neg A \imp A) \imp A) \imp (A \imp \neg A \imp A) \imp (\neg A \imp A \iff A)
(\neg A \imp A) \imp A
(A \imp \neg A \imp A) \imp (\neg A \imp A \iff A)
A \imp \neg A \imp A
\neg A \imp A \iff A
A \or A \iff A

Step	Hyp	Ref	Expression
1		iff_comp	((\neg A \imp A) \imp A) \imp (A \imp \neg A \imp A) \imp (\neg A \imp A \iff A)
2		neg_imp_tosame	(\neg A \imp A) \imp A
3	1, 2	ax_mp	(A \imp \neg A \imp A) \imp (\neg A \imp A \iff A)
4		introl_imp	A \imp \neg A \imp A
5	3, 4	ax_mp	\neg A \imp A \iff A
6	5	conv or	A \or A \iff A

Axiom use

Logic (ax_mp, ax_1, ax_2, ax_3)