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 591. (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 593 | . 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 589 |
This theorem is referenced by: pm2.21fal 1336 pm2.21ddne 2368 ordtriexmidlem 4405 ordtri2or2exmidlem 4411 onsucelsucexmidlem 4414 wetriext 4461 reg3exmidlemwe 4463 nntr2 6367 nnm00 6393 phpm 6727 fidifsnen 6732 dif1enen 6742 infnfi 6757 en2eqpr 6769 aptiprleml 7415 aptiprlemu 7416 uzdisj 9841 nn0disj 9883 addmodlteq 10139 frec2uzlt2d 10145 iseqf1olemab 10230 iseqf1olemmo 10233 hashennnuni 10493 hashfiv01gt1 10496 xrmaxiflemab 10984 xrmaxiflemlub 10985 xrmaxltsup 10995 xrbdtri 11013 divalglemeunn 11545 divalglemeuneg 11547 zsupcllemex 11566 ennnfonelemk 11840 cnplimclemle 12733 trilpolemlt1 13161 |
Copyright terms: Public domain | W3C validator |