![]() |
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 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: ![]() ![]() |
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 1346 pclem6 1353 nfnth 1442 alnex 1476 ax4sp1 1514 rex0 3385 0ss 3406 abf 3411 ral0 3469 int0 3793 nnsucelsuc 6395 nnmordi 6420 nnaordex 6431 0er 6471 fiintim 6825 elnnnn0b 9045 xltnegi 9648 xnn0xadd0 9680 frec2uzltd 10207 sum0 11189 fsum2dlemstep 11235 nn0enne 11635 exprmfct 11854 0met 12592 |
Copyright terms: Public domain | W3C validator |