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 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 3407 csbprc 3408 rzal 3460 poirr2 4931 nnsucuniel 6391 nnawordex 6424 swoord2 6459 difinfsnlem 6984 exmidomni 7014 elni2 7122 cauappcvgprlemdisj 7459 caucvgprlemdisj 7482 caucvgprprlemdisj 7510 caucvgsr 7610 lelttr 7852 nnsub 8759 nn0ge2m1nn 9037 elnnz 9064 elnn0z 9067 indstr 9388 indstr2 9403 xrltnsym 9579 xrlttr 9581 xrltso 9582 xrlelttr 9589 xltnegi 9618 xsubge0 9664 ixxdisj 9686 icodisj 9775 fzm1 9880 qbtwnxr 10035 frec2uzlt2d 10177 facdiv 10484 resqrexlemgt0 10792 climuni 11062 fsumcl2lem 11167 dvdsle 11542 prmdvdsexpr 11828 prmfac1 11830 sqrt2irr 11840 phibndlem 11892 isxmet2d 12517 trilpolemres 13235 |
Copyright terms: Public domain | W3C validator |