Theorem explosion ≪ | index | src | ≫

爆炸原理

theorem explosion (A: wff): $ \false \imp A $;
StepHypRefExpression
1 neg_elimintror_imp 
\neg \false \imp \false \imp A
2 negfalse_proof 
\neg \false
3 1, 2 ax_mp 
\false \imp A

Axiom use

Logic (ax_mp, ax_1, ax_2, ax_3)