Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > pm2.21i | Unicode version |
Description: A contradiction implies anything. Inference from pm2.21 591. (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 591 | . 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 589 |
This theorem is referenced by: pm2.24ii 621 2false 675 pm3.2ni 787 falim 1330 pclem6 1337 nfnth 1426 alnex 1460 ax4sp1 1498 rex0 3350 0ss 3371 abf 3376 ral0 3434 int0 3755 nnsucelsuc 6355 nnmordi 6380 nnaordex 6391 0er 6431 fiintim 6785 elnnnn0b 8989 xltnegi 9586 xnn0xadd0 9618 frec2uzltd 10144 sum0 11125 fsum2dlemstep 11171 nn0enne 11526 exprmfct 11745 0met 12480 |
Copyright terms: Public domain | W3C validator |