Theorem assgin_true ≪ | index | src | ≫

赋值为真

theorem assgin_true (A: wff): $ A \iff A \iff \true $;


(A \imp (A \iff \true)) \imp ((A \iff \true) \imp A) \imp (A \iff A \iff \true)
A \imp (A \iff \true)
((A \iff \true) \imp A) \imp (A \iff A \iff \true)
((A \iff \true) \imp \true \imp A) \imp (\true \imp A \iff A) \imp (A \iff \true) \imp A
(A \iff \true) \imp \true \imp A
(\true \imp A \iff A) \imp (A \iff \true) \imp A
\true \imp A \iff A
(A \iff \true) \imp A
A \iff A \iff \true

Step	Hyp	Ref	Expression
1		iff_comp	(A \imp (A \iff \true)) \imp ((A \iff \true) \imp A) \imp (A \iff A \iff \true)
2		prov_iff_true	A \imp (A \iff \true)
3	1, 2	ax_mp	((A \iff \true) \imp A) \imp (A \iff A \iff \true)
4		imp_iff_tran_imp	((A \iff \true) \imp \true \imp A) \imp (\true \imp A \iff A) \imp (A \iff \true) \imp A
5		iff_decompbwd	(A \iff \true) \imp \true \imp A
6	4, 5	ax_mp	(\true \imp A \iff A) \imp (A \iff \true) \imp A
7		trueimp_eqv_self	\true \imp A \iff A
8	6, 7	ax_mp	(A \iff \true) \imp A
9	3, 8	ax_mp	A \iff A \iff \true

Axiom use

Logic (ax_mp, ax_1, ax_2, ax_3)