![]() |
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 618. (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 618 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | ax-mp 5 |
1
![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-in2 616 |
This theorem is referenced by: pm2.24ii 648 2false 702 pm3.2ni 814 falim 1378 pclem6 1385 nfnth 1476 alnex 1510 ax4sp1 1544 rex0 3455 0ss 3476 abf 3481 ral0 3539 int0 3873 nnsucelsuc 6516 nnmordi 6541 nnaordex 6553 0er 6593 fiintim 6957 elnnnn0b 9250 xltnegi 9865 xnn0xadd0 9897 frec2uzltd 10434 sum0 11428 fsum2dlemstep 11474 prod0 11625 fprod2dlemstep 11662 nn0enne 11939 exprmfct 12170 prm23lt5 12295 4sqlem18 12440 0met 14344 lgsdir2lem3 14892 2lgsoddprmlem3 14920 |
Copyright terms: Public domain | W3C validator |