![]() |
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 617. (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 617 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | syl 14 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-in2 615 |
This theorem is referenced by: pm2.21dd 620 pm5.21 695 2falsed 702 mtord 783 prlem1 973 eq0rdv 3467 csbprc 3468 rzal 3520 poirr2 5017 nnsucuniel 6490 nnawordex 6524 swoord2 6559 difinfsnlem 7092 exmidomni 7134 elni2 7301 cauappcvgprlemdisj 7638 caucvgprlemdisj 7661 caucvgprprlemdisj 7689 caucvgsr 7789 lelttr 8033 nnsub 8944 nn0ge2m1nn 9222 elnnz 9249 elnn0z 9252 indstr 9579 indstr2 9595 xrltnsym 9777 xrlttr 9779 xrltso 9780 xrlelttr 9790 xltnegi 9819 xsubge0 9865 ixxdisj 9887 icodisj 9976 fzm1 10083 qbtwnxr 10241 frec2uzlt2d 10387 nn0ltexp2 10671 facdiv 10699 resqrexlemgt0 11010 climuni 11282 fsumcl2lem 11387 dvdsle 11830 prmdvdsexpr 12130 prmfac1 12132 sqrt2irr 12142 phibndlem 12196 dvdsprmpweqle 12316 isxmet2d 13512 lgsdir2lem2 14094 trilpolemres 14443 |
Copyright terms: Public domain | W3C validator |