![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > pm2.21dd | GIF version |
Description: A contradiction implies anything. Deduction from pm2.21 617. (Contributed by Mario Carneiro, 9-Feb-2017.) |
Ref | Expression |
---|---|
pm2.21dd.1 | ⊢ (𝜑 → 𝜓) |
pm2.21dd.2 | ⊢ (𝜑 → ¬ 𝜓) |
Ref | Expression |
---|---|
pm2.21dd | ⊢ (𝜑 → 𝜒) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pm2.21dd.1 | . 2 ⊢ (𝜑 → 𝜓) | |
2 | pm2.21dd.2 | . . 3 ⊢ (𝜑 → ¬ 𝜓) | |
3 | 2 | pm2.21d 619 | . 2 ⊢ (𝜑 → (𝜓 → 𝜒)) |
4 | 1, 3 | mpd 13 | 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.21fal 1373 pm2.21ddne 2430 ordtriexmidlem 4520 ordtri2or2exmidlem 4527 onsucelsucexmidlem 4530 wetriext 4578 reg3exmidlemwe 4580 nntr2 6506 nnm00 6533 phpm 6867 fidifsnen 6872 dif1enen 6882 infnfi 6897 en2eqpr 6909 aptiprleml 7640 aptiprlemu 7641 uzdisj 10095 nn0disj 10140 addmodlteq 10400 frec2uzlt2d 10406 iseqf1olemab 10491 iseqf1olemmo 10494 hashennnuni 10761 hashfiv01gt1 10764 xrmaxiflemab 11257 xrmaxiflemlub 11258 xrmaxltsup 11268 xrbdtri 11286 divalglemeunn 11928 divalglemeuneg 11930 zsupcllemex 11949 ennnfonelemk 12403 cnplimclemle 14222 efltlemlt 14280 trilpolemlt1 14874 neapmkvlem 14900 |
Copyright terms: Public domain | W3C validator |