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 612. (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 612 | . 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 610 |
This theorem is referenced by: pm2.24ii 642 2false 696 pm3.2ni 808 falim 1362 pclem6 1369 nfnth 1458 alnex 1492 ax4sp1 1526 rex0 3432 0ss 3453 abf 3458 ral0 3516 int0 3845 nnsucelsuc 6470 nnmordi 6495 nnaordex 6507 0er 6547 fiintim 6906 elnnnn0b 9179 xltnegi 9792 xnn0xadd0 9824 frec2uzltd 10359 sum0 11351 fsum2dlemstep 11397 prod0 11548 fprod2dlemstep 11585 nn0enne 11861 exprmfct 12092 prm23lt5 12217 0met 13178 lgsdir2lem3 13725 |
Copyright terms: Public domain | W3C validator |