Theorem impfalse_eqv_negself ≪ | index | src | ≫

\imp\false等价\neg自身

theorem impfalse_eqv_negself (A: wff): $ A \imp \false \iff \neg A $;
StepHypRefExpression
1 iff_comp 
((A \imp \false) \imp \neg A) \imp (\neg A \imp A \imp \false) \imp (A \imp \false \iff \neg A)
2 imp_tran 
((A \imp \false) \imp A \imp \neg A) \imp ((A \imp \neg A) \imp \neg A) \imp (A \imp \false) \imp \neg A
3 imp_introl_imp 
(\false \imp \neg A) \imp (A \imp \false) \imp A \imp \neg A
4 explosion 
\false \imp \neg A
5 3, 4 ax_mp 
(A \imp \false) \imp A \imp \neg A
6 2, 5 ax_mp 
((A \imp \neg A) \imp \neg A) \imp (A \imp \false) \imp \neg A
7 imp_neg_tosame_neg 
(A \imp \neg A) \imp \neg A
8 6, 7 ax_mp 
(A \imp \false) \imp \neg A
9 1, 8 ax_mp 
(\neg A \imp A \imp \false) \imp (A \imp \false \iff \neg A)
10 neg_elimintror_imp 
\neg A \imp A \imp \false
11 9, 10 ax_mp 
A \imp \false \iff \neg A

Axiom use

Logic (ax_mp, ax_1, ax_2, ax_3)