| 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 697 2falsed 704 mtord 785 prlem1 976 eq0rdv 3509 csbprc 3510 rzal 3562 poirr2 5089 nnsucuniel 6599 nnawordex 6633 swoord2 6668 difinfsnlem 7222 exmidomni 7265 elni2 7457 cauappcvgprlemdisj 7794 caucvgprlemdisj 7817 caucvgprprlemdisj 7845 caucvgsr 7945 lelttr 8191 nnsub 9105 nn0ge2m1nn 9385 elnnz 9412 elnn0z 9415 indstr 9744 indstr2 9760 xrltnsym 9945 xrlttr 9947 xrltso 9948 xrlelttr 9958 xltnegi 9987 xsubge0 10033 ixxdisj 10055 icodisj 10144 fzm1 10252 qbtwnxr 10432 frec2uzlt2d 10581 nn0ltexp2 10886 facdiv 10915 resqrexlemgt0 11416 climuni 11689 fsumcl2lem 11794 dvdsle 12240 prmdvdsexpr 12557 prmfac1 12559 sqrt2irr 12569 phibndlem 12623 dvdsprmpweqle 12745 isxmet2d 14905 lgsdir2lem2 15591 lgseisenlem2 15633 trilpolemres 16153 |
| Copyright terms: Public domain | W3C validator |