![]() |
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 618. (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 618 |
. 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 616 |
This theorem is referenced by: pm2.21dd 621 pm5.21 696 2falsed 703 mtord 784 prlem1 975 eq0rdv 3482 csbprc 3483 rzal 3535 poirr2 5039 nnsucuniel 6521 nnawordex 6555 swoord2 6590 difinfsnlem 7129 exmidomni 7171 elni2 7344 cauappcvgprlemdisj 7681 caucvgprlemdisj 7704 caucvgprprlemdisj 7732 caucvgsr 7832 lelttr 8077 nnsub 8989 nn0ge2m1nn 9267 elnnz 9294 elnn0z 9297 indstr 9625 indstr2 9641 xrltnsym 9825 xrlttr 9827 xrltso 9828 xrlelttr 9838 xltnegi 9867 xsubge0 9913 ixxdisj 9935 icodisj 10024 fzm1 10132 qbtwnxr 10290 frec2uzlt2d 10437 nn0ltexp2 10724 facdiv 10753 resqrexlemgt0 11064 climuni 11336 fsumcl2lem 11441 dvdsle 11885 prmdvdsexpr 12185 prmfac1 12187 sqrt2irr 12197 phibndlem 12251 dvdsprmpweqle 12372 isxmet2d 14325 lgsdir2lem2 14908 lgseisenlem2 14929 trilpolemres 15269 |
Copyright terms: Public domain | W3C validator |