Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > pm2.21fal | GIF version |
Description: If a wff and its negation are provable, then falsum is provable. (Contributed by Mario Carneiro, 9-Feb-2017.) |
Ref | Expression |
---|---|
pm2.21fal.1 | ⊢ (𝜑 → 𝜓) |
pm2.21fal.2 | ⊢ (𝜑 → ¬ 𝜓) |
Ref | Expression |
---|---|
pm2.21fal | ⊢ (𝜑 → ⊥) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pm2.21fal.1 | . 2 ⊢ (𝜑 → 𝜓) | |
2 | pm2.21fal.2 | . 2 ⊢ (𝜑 → ¬ 𝜓) | |
3 | 1, 2 | pm2.21dd 615 | 1 ⊢ (𝜑 → ⊥) |
Colors of variables: wff set class |
Syntax hints: ¬ wn 3 → wi 4 ⊥wfal 1353 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-in2 610 |
This theorem is referenced by: genpdisj 7478 suplocexprlemdisj 7675 suplocexprlemub 7678 suplocsrlem 7763 recvguniqlem 10951 resqrexlemoverl 10978 leabs 11031 climge0 11281 isprm5lem 12088 dedekindeulemeu 13359 dedekindicclemeu 13368 pw1nct 14001 |
Copyright terms: Public domain | W3C validator |