![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > pm2.21d | GIF version |
Description: A contradiction implies anything. Deduction from pm2.21 580. (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 580 | . 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-1 5 ax-2 6 ax-mp 7 ax-in2 578 |
This theorem is referenced by: pm2.21dd 583 pm5.21 644 2falsed 651 mtord 730 prlem1 915 eq0rdv 3304 csbprc 3305 rzal 3355 poirr2 4767 nnsucuniel 6159 nnawordex 6188 swoord2 6223 elni2 6618 cauappcvgprlemdisj 6955 caucvgprlemdisj 6978 caucvgprprlemdisj 7006 caucvgsr 7092 lelttr 7318 nnsub 8196 nn0ge2m1nn 8467 elnnz 8494 elnn0z 8497 indstr 8814 indstr2 8829 xrltnsym 8996 xrlttr 8998 xrltso 8999 xrlelttr 9004 xltnegi 9030 ixxdisj 9054 icodisj 9142 fzm1 9245 qbtwnxr 9396 frec2uzlt2d 9538 expival 9627 facdiv 9814 resqrexlemgt0 10107 climuni 10333 dvdsle 10452 prmdvdsexpr 10736 prmfac1 10738 sqrt2irr 10748 phibndlem 10799 |
Copyright terms: Public domain | W3C validator |