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 612. (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 612 | . 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 610 |
This theorem is referenced by: pm2.21dd 615 pm5.21 690 2falsed 697 mtord 778 prlem1 968 eq0rdv 3459 csbprc 3460 rzal 3512 poirr2 5003 nnsucuniel 6474 nnawordex 6508 swoord2 6543 difinfsnlem 7076 exmidomni 7118 elni2 7276 cauappcvgprlemdisj 7613 caucvgprlemdisj 7636 caucvgprprlemdisj 7664 caucvgsr 7764 lelttr 8008 nnsub 8917 nn0ge2m1nn 9195 elnnz 9222 elnn0z 9225 indstr 9552 indstr2 9568 xrltnsym 9750 xrlttr 9752 xrltso 9753 xrlelttr 9763 xltnegi 9792 xsubge0 9838 ixxdisj 9860 icodisj 9949 fzm1 10056 qbtwnxr 10214 frec2uzlt2d 10360 nn0ltexp2 10644 facdiv 10672 resqrexlemgt0 10984 climuni 11256 fsumcl2lem 11361 dvdsle 11804 prmdvdsexpr 12104 prmfac1 12106 sqrt2irr 12116 phibndlem 12170 dvdsprmpweqle 12290 isxmet2d 13142 lgsdir2lem2 13724 trilpolemres 14074 |
Copyright terms: Public domain | W3C validator |