Theorem prov_iff_true ≪ | index | src | ≫

定理与\true等价

theorem prov_iff_true (A: wff): $ A \imp (A \iff \true) $;


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

Step	Hyp	Ref	Expression
1		iff_comp	(A \imp \true) \imp (\true \imp A) \imp (A \iff \true)
2	1	_hyp_null_complete	A \imp (A \imp \true) \imp (\true \imp A) \imp (A \iff \true)
3		introl_imp	\true \imp A \imp \true
4	3	_hyp_null_complete	A \imp \true \imp A \imp \true
5		true_proof	\true
6	5	_hyp_null_complete	A \imp \true
7	4, 6	_hyp_mp	A \imp A \imp \true
8	2, 7	_hyp_mp	A \imp (\true \imp A) \imp (A \iff \true)
9		introl_imp	A \imp \true \imp A
10	9	_hyp_null_complete	A \imp A \imp \true \imp A
11		_hyp_null_intro	A \imp A
12	10, 11	_hyp_mp	A \imp \true \imp A
13	8, 12	_hyp_mp	A \imp (A \iff \true)

Axiom use

Logic (ax_mp, ax_1, ax_2, ax_3)