Theorem assign_false ≪ | index | src | ≫

赋值为假

theorem assign_false (A: wff): $ \neg A \iff A \iff \false $;
StepHypRefExpression
1 iff_comp 
(\neg A \imp (A \iff \false)) \imp ((A \iff \false) \imp \neg A) \imp (\neg A \iff A \iff \false)
2 provneg_iff_false 
\neg A \imp (A \iff \false)
3 1, 2 ax_mp 
((A \iff \false) \imp \neg A) \imp (\neg A \iff A \iff \false)
4 imp_iff_tran_imp 
((A \iff \false) \imp A \imp \false) \imp (A \imp \false \iff \neg A) \imp (A \iff \false) \imp \neg A
5 iff_decomp 
(A \iff \false) \imp A \imp \false
6 4, 5 ax_mp 
(A \imp \false \iff \neg A) \imp (A \iff \false) \imp \neg A
7 impfalse_eqv_negself 
A \imp \false \iff \neg A
8 6, 7 ax_mp 
(A \iff \false) \imp \neg A
9 3, 8 ax_mp 
\neg A \iff A \iff \false

Axiom use

Logic (ax_mp, ax_1, ax_2, ax_3)