Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > pm2.21i | GIF version |
Description: A contradiction implies anything. Inference from pm2.21 607. (Contributed by NM, 16-Sep-1993.) (Revised by Mario Carneiro, 31-Jan-2015.) |
Ref | Expression |
---|---|
pm2.21i.1 | ⊢ ¬ 𝜑 |
Ref | Expression |
---|---|
pm2.21i | ⊢ (𝜑 → 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pm2.21i.1 | . 2 ⊢ ¬ 𝜑 | |
2 | pm2.21 607 | . 2 ⊢ (¬ 𝜑 → (𝜑 → 𝜓)) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ (𝜑 → 𝜓) |
Colors of variables: wff set class |
Syntax hints: ¬ wn 3 → wi 4 |
This theorem was proved from axioms: ax-mp 5 ax-in2 605 |
This theorem is referenced by: pm2.24ii 637 2false 691 pm3.2ni 803 falim 1349 pclem6 1356 nfnth 1445 alnex 1479 ax4sp1 1513 rex0 3412 0ss 3433 abf 3438 ral0 3496 int0 3823 nnsucelsuc 6440 nnmordi 6465 nnaordex 6476 0er 6516 fiintim 6875 elnnnn0b 9139 xltnegi 9745 xnn0xadd0 9777 frec2uzltd 10311 sum0 11296 fsum2dlemstep 11342 prod0 11493 fprod2dlemstep 11530 nn0enne 11805 exprmfct 12030 prm23lt5 12153 0met 12854 |
Copyright terms: Public domain | W3C validator |