Theorem wff_or_true_iff_true ≪ | index | src | ≫

\or真值表：wff \or \true \iff \true

theorem wff_or_true_iff_true (A: wff): $ A \or \true \iff \true $;


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

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

Axiom use

Logic (ax_mp, ax_1, ax_2, ax_3)