![]() |
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 3412 csbprc 3413 rzal 3465 poirr2 4939 nnsucuniel 6399 nnawordex 6432 swoord2 6467 difinfsnlem 6992 exmidomni 7022 elni2 7146 cauappcvgprlemdisj 7483 caucvgprlemdisj 7506 caucvgprprlemdisj 7534 caucvgsr 7634 lelttr 7876 nnsub 8783 nn0ge2m1nn 9061 elnnz 9088 elnn0z 9091 indstr 9415 indstr2 9430 xrltnsym 9609 xrlttr 9611 xrltso 9612 xrlelttr 9619 xltnegi 9648 xsubge0 9694 ixxdisj 9716 icodisj 9805 fzm1 9911 qbtwnxr 10066 frec2uzlt2d 10208 facdiv 10516 resqrexlemgt0 10824 climuni 11094 fsumcl2lem 11199 dvdsle 11578 prmdvdsexpr 11864 prmfac1 11866 sqrt2irr 11876 phibndlem 11928 isxmet2d 12556 trilpolemres 13410 |
Copyright terms: Public domain | W3C validator |