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 607. (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 607 | . 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 605 |
This theorem is referenced by: pm2.21dd 610 pm5.21 685 2falsed 692 mtord 773 prlem1 958 eq0rdv 3438 csbprc 3439 rzal 3491 poirr2 4979 nnsucuniel 6443 nnawordex 6476 swoord2 6511 difinfsnlem 7044 exmidomni 7086 elni2 7235 cauappcvgprlemdisj 7572 caucvgprlemdisj 7595 caucvgprprlemdisj 7623 caucvgsr 7723 lelttr 7966 nnsub 8873 nn0ge2m1nn 9151 elnnz 9178 elnn0z 9181 indstr 9505 indstr2 9521 xrltnsym 9701 xrlttr 9703 xrltso 9704 xrlelttr 9711 xltnegi 9740 xsubge0 9786 ixxdisj 9808 icodisj 9897 fzm1 10003 qbtwnxr 10161 frec2uzlt2d 10307 facdiv 10616 resqrexlemgt0 10924 climuni 11194 fsumcl2lem 11299 dvdsle 11740 prmdvdsexpr 12029 prmfac1 12031 sqrt2irr 12041 phibndlem 12095 isxmet2d 12790 trilpolemres 13655 |
Copyright terms: Public domain | W3C validator |