Theorem wff_and_false_iff_false ≪ | index | src | ≫

\and真值表：wff \and \false \iff \false

theorem wff_and_false_iff_false (A: wff): $ A \and \false \iff \false $;
StepHypRefExpression
1 iff_intro_neg 
(A \imp \neg \false \iff \true) \imp (\neg (A \imp \neg \false) \iff \neg \true)
2 prov_iff_true 
(A \imp \neg \false) \imp (A \imp \neg \false \iff \true)
3 imp_tran 
(A \imp \true) \imp (\true \imp \neg \neg \true) \imp A \imp \neg \neg \true
4 true_comp 
A \imp \true
5 3, 4 ax_mp 
(\true \imp \neg \neg \true) \imp A \imp \neg \neg \true
6 negneg_intro 
\true \imp \neg \neg \true
7 5, 6 ax_mp 
A \imp \neg \neg \true
8 7 conv false 
A \imp \neg \false
9 2, 8 ax_mp 
A \imp \neg \false \iff \true
10 1, 9 ax_mp 
\neg (A \imp \neg \false) \iff \neg \true
11 10 conv false 
\neg (A \imp \neg \false) \iff \false
12 11 conv and 
A \and \false \iff \false

Axiom use

Logic (ax_mp, ax_1, ax_2, ax_3)