![]() |
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 585. (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 585 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | ax-mp 7 |
1
![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() |
This theorem was proved from axioms: ax-mp 7 ax-in2 583 |
This theorem is referenced by: pm2.24ii 614 2false 655 pm3.2ni 765 falim 1310 pclem6 1317 nfnth 1406 alnex 1440 ax4sp1 1478 rex0 3319 0ss 3340 abf 3345 ral0 3403 int0 3724 nnsucelsuc 6292 nnmordi 6315 nnaordex 6326 0er 6366 fiintim 6719 elnnnn0b 8815 xltnegi 9401 xnn0xadd0 9433 frec2uzltd 9959 sum0 10947 fsum2dlemstep 10993 nn0enne 11345 exprmfct 11562 0met 12186 |
Copyright terms: Public domain | W3C validator |