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 606. (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 606 | . 2 | |
3 | 1, 2 | syl 14 | 1 |
Colors of variables: wff set class |
Syntax hints: wn 3 wi 4 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-in2 604 |
This theorem is referenced by: pm2.21dd 609 pm5.21 684 2falsed 691 mtord 772 prlem1 957 eq0rdv 3402 csbprc 3403 rzal 3455 poirr2 4926 nnsucuniel 6384 nnawordex 6417 swoord2 6452 difinfsnlem 6977 exmidomni 7007 elni2 7115 cauappcvgprlemdisj 7452 caucvgprlemdisj 7475 caucvgprprlemdisj 7503 caucvgsr 7603 lelttr 7845 nnsub 8752 nn0ge2m1nn 9030 elnnz 9057 elnn0z 9060 indstr 9381 indstr2 9396 xrltnsym 9572 xrlttr 9574 xrltso 9575 xrlelttr 9582 xltnegi 9611 xsubge0 9657 ixxdisj 9679 icodisj 9768 fzm1 9873 qbtwnxr 10028 frec2uzlt2d 10170 facdiv 10477 resqrexlemgt0 10785 climuni 11055 fsumcl2lem 11160 dvdsle 11531 prmdvdsexpr 11817 prmfac1 11819 sqrt2irr 11829 phibndlem 11881 isxmet2d 12506 trilpolemres 13224 |
Copyright terms: Public domain | W3C validator |