![]() |
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 587. (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 589 | . 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-1 5 ax-2 6 ax-mp 7 ax-in2 585 |
This theorem is referenced by: pm2.21fal 1319 pm2.21ddne 2350 ordtriexmidlem 4373 ordtri2or2exmidlem 4379 onsucelsucexmidlem 4382 wetriext 4429 reg3exmidlemwe 4431 nntr2 6329 nnm00 6355 phpm 6688 fidifsnen 6693 dif1enen 6703 infnfi 6718 en2eqpr 6730 aptiprleml 7348 aptiprlemu 7349 uzdisj 9714 nn0disj 9756 addmodlteq 10012 frec2uzlt2d 10018 iseqf1olemab 10103 iseqf1olemmo 10106 hashennnuni 10366 hashfiv01gt1 10369 xrmaxiflemab 10855 xrmaxiflemlub 10856 xrmaxltsup 10866 xrbdtri 10884 divalglemeunn 11413 divalglemeuneg 11415 zsupcllemex 11434 ennnfonelemk 11705 trilpolemlt1 12818 |
Copyright terms: Public domain | W3C validator |