![]() |
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 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: ¬ wn 3 → wi 4 |
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 5021 nnsucuniel 6495 nnawordex 6529 swoord2 6564 difinfsnlem 7097 exmidomni 7139 elni2 7312 cauappcvgprlemdisj 7649 caucvgprlemdisj 7672 caucvgprprlemdisj 7700 caucvgsr 7800 lelttr 8044 nnsub 8956 nn0ge2m1nn 9234 elnnz 9261 elnn0z 9264 indstr 9591 indstr2 9607 xrltnsym 9791 xrlttr 9793 xrltso 9794 xrlelttr 9804 xltnegi 9833 xsubge0 9879 ixxdisj 9901 icodisj 9990 fzm1 10097 qbtwnxr 10255 frec2uzlt2d 10401 nn0ltexp2 10685 facdiv 10713 resqrexlemgt0 11024 climuni 11296 fsumcl2lem 11401 dvdsle 11844 prmdvdsexpr 12144 prmfac1 12146 sqrt2irr 12156 phibndlem 12210 dvdsprmpweqle 12330 isxmet2d 13741 lgsdir2lem2 14323 trilpolemres 14672 |
Copyright terms: Public domain | W3C validator |