Theorem true_imp_false_iff_false ≪ | index | src | ≫

\imp真值表：\true \imp \false \iff \false

theorem true_imp_false_iff_false: $ \true \imp \false \iff \false $;
StepHypRefExpression
1 iff_comp 
((\true \imp \neg \true) \imp \neg \true) \imp (\neg \true \imp \true \imp \neg \true) \imp (\true \imp \neg \true \iff \neg \true)
2 imp_neg_tosame_neg 
(\true \imp \neg \true) \imp \neg \true
3 1, 2 ax_mp 
(\neg \true \imp \true \imp \neg \true) \imp (\true \imp \neg \true \iff \neg \true)
4 introl_imp 
\neg \true \imp \true \imp \neg \true
5 3, 4 ax_mp 
\true \imp \neg \true \iff \neg \true
6 5 conv false 
\true \imp \false \iff \false

Axiom use

Logic (ax_mp, ax_1, ax_2, ax_3)