![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > pm2.21d | Unicode version |
Description: A contradiction implies anything. Deduction from pm2.21 547. (Contributed by NM, 10-Feb-1996.) |
Ref | Expression |
---|---|
pm2.21d.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
pm2.21d |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pm2.21d.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | pm2.21 547 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | syl 14 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-in2 545 |
This theorem is referenced by: pm2.21dd 550 pm5.21 610 2falsed 617 mtord 696 prlem1 879 eq0rdv 3255 csbprc 3256 rzal 3312 poirr2 4660 nnawordex 6037 swoord2 6072 elni2 6298 cauappcvgprlemdisj 6623 caucvgprlemdisj 6645 lelttr 6903 nnsub 7733 nn0ge2m1nn 8018 elnnz 8031 elnn0z 8034 indstr 8312 indstr2 8322 xrltnsym 8484 xrlttr 8486 xrltso 8487 xrlelttr 8492 xltnegi 8518 ixxdisj 8542 icodisj 8630 fzm1 8732 frec2uzlt2d 8871 expival 8911 |
Copyright terms: Public domain | W3C validator |