Theorem false_imp_wff_iff_true ≪ | index | src | ≫

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

theorem false_imp_wff_iff_true (A: wff): $ \false \imp A \iff \true $;
StepHypRefExpression
1 iff_tran 
(\neg \true \imp A \iff \neg A \imp \true) \imp (\neg A \imp \true \iff \true) \imp (\neg \true \imp A \iff \true)
2 neg_imp_perm 
\neg \true \imp A \iff \neg A \imp \true
3 1, 2 ax_mp 
(\neg A \imp \true \iff \true) \imp (\neg \true \imp A \iff \true)
4 wff_imp_true_iff_true 
\neg A \imp \true \iff \true
5 3, 4 ax_mp 
\neg \true \imp A \iff \true
6 5 conv false 
\false \imp A \iff \true

Axiom use

Logic (ax_mp, ax_1, ax_2, ax_3)